Validate Proof command: runs typing.ml on the current proof

doc/tools/docgram/fullGrammar

@@ -520,6 +520,7 @@ command: [
 | "Show" "Intros"
 | "Show" "Match" reference
 | "Guarded"
+| "Validate" "Proof"
 | "Create" "HintDb" IDENT; [ "discriminated" | ]
 | "Remove" "Hints" LIST1 global opt_hintbases
 | "Hint" hint opt_hintbases

doc/tools/docgram/orderedGrammar

@@ -818,6 +818,7 @@ command: [
 | "Show" "Intros"
 | "Show" "Match" qualid
 | "Guarded"
+| "Validate" "Proof"
 | "Create" "HintDb" ident OPT "discriminated"
 | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
 | "Comments" LIST0 [ one_term | string | natural ]

vernac/g_proofs.mlg

@@ -95,6 +95,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Show"; IDENT "Intros" -> { VernacSynPure (VernacShow (ShowIntros true)) }
       | IDENT "Show"; IDENT "Match"; id = reference -> { VernacSynPure (VernacShow (ShowMatch id)) }
       | IDENT "Guarded" -> { VernacSynPure VernacCheckGuard }
+      | IDENT "Validate"; IDENT "Proof" -> { VernacSynPure VernacValidateProof }
       (* Hints for Auto and EAuto *)
       | IDENT "Create"; IDENT "HintDb" ;
           id = IDENT ; b = [ IDENT "discriminated" -> { true } | -> { false } ] ->

vernac/ppvernac.ml

@@ -724,6 +724,8 @@ let pr_synpure_vernac_expr v =
   | VernacCheckGuard ->
     return (keyword "Guarded")
 
+  | VernacValidateProof -> return (keyword "Validate Proof")
+
   (* Resetting *)
   | VernacResetName id ->
     return (keyword "Reset" ++ spc() ++ pr_lident id)

vernac/vernac_classifier.ml

@@ -100,7 +100,7 @@ let classify_vernac e =
     | VernacProof _
     | VernacFocus _ | VernacUnfocus
     | VernacSubproof _
-    | VernacCheckGuard
+    | VernacCheckGuard | VernacValidateProof
     | VernacUnfocused
     | VernacBullet _ ->
         VtProofStep { proof_block_detection = Some "bullet" }

vernac/vernacentries.ml

@@ -2108,6 +2108,44 @@ let vernac_check_guard ~pstate =
   let env = Environ.reset_with_named_context hyps (Global.env ()) in
   Inductiveops.control_only_guard env sigma pfterm;
   str "The condition holds up to here."
+let vernac_validate_proof ~pstate =
+  let pts = Declare.Proof.get pstate in
+  let { Proof.entry; Proof.sigma } = Proof.data pts in
+  let hyps, pfterm, pftyp = List.hd (Proofview.initial_goals entry) in
+  (* XXX can the initial hyps contain something broken? For now assume they're correct.
+     NB: in the "Lemma foo args : bla." case the args are part of the
+     term and intro'd after the proof is opened. Only the section
+     variables are in the hyps. *)
+  let env = Environ.reset_with_named_context hyps (Global.env ()) in
+  let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
+  let sigma' = Typing.check env sigma pfterm pftyp in
+  let evar_issues =
+    (* Use Evar.Map.merge as a kind of for_all2 *)
+    Evar.Map.merge (fun e orig now -> match orig, now with
+        | None, None -> assert false
+        | Some _, Some _ -> None (* assume same *)
+        | Some evi, None ->
+          let EvarInfo evi' = Evd.find sigma' e in
+          let body = match Evd.evar_body evi' with
+            | Evar_empty -> assert false
+            | Evar_defined body -> body
+          in
+          Some
+            Pp.(str "Evar " ++ Printer.pr_evar sigma (e, evi)
+                ++ spc() ++ str "was inferred by unification to be" ++ spc()
+                ++ pr_econstr_env (Evd.evar_env env evi') sigma' body)
+        | None, Some _ -> (* ignore new evar *)
+          assert (not (Evd.is_defined sigma e));
+          None
+      )
+      (Evd.undefined_map sigma)
+      (Evd.undefined_map sigma')
+  in
+  (* TODO check ustate *)
+
+  if Evar.Map.is_empty evar_issues then
+    str "No issues found."
+  else prlist_with_sep fnl snd (Evar.Map.bindings evar_issues)
 
 let translate_vernac_synterp ?loc ~atts v = let open Vernacextend in match v with
   | EVernacNotation { local; decl } ->
@@ -2429,6 +2467,10 @@ let translate_pure_vernac ?loc ~atts v = let open Vernacextend in match v with
     vtreadproof(fun ~pstate ->
         unsupported_attributes atts;
         Feedback.msg_notice @@ vernac_check_guard ~pstate)
+  | VernacValidateProof ->
+    vtreadproof(fun ~pstate ->
+        unsupported_attributes atts;
+        Feedback.msg_notice @@ vernac_validate_proof ~pstate)
   | VernacProof (tac, using) ->
     vtmodifyproof(fun ~pstate ->
     unsupported_attributes atts;

vernac/vernacexpr.mli

@@ -486,6 +486,7 @@ type nonrec synpure_vernac_expr =
   | VernacEndSubproof
   | VernacShow of showable
   | VernacCheckGuard
+  | VernacValidateProof
   | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
 
   | VernacAddOption of Goptions.option_name * Goptions.table_value list