Merge PR #9129: [proof] Removal of imperative state ; interpretation layers only.

Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes

1 files changed, 28 insertions, 19 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 2f00b41b7c..2aadbd224f 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,7 +255,8 @@ let interp_fixpoint ~cofix l ntns =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+  let pstate =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -265,8 +266,9 @@ let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximp
       Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
     let evd = Evd.from_ctx ctx in
-    Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
-      evd pl (Some(false,indexes,init_tac)) thms None
+    Some
+    (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint)
+      evd pl (Some(false,indexes,init_tac)) thms None)
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -282,15 +284,18 @@ let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximp
     let ctx = Evd.check_univ_decl ~poly evd pl in
     let pl = Evd.universe_binders evd in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
-    ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
+    ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, Fixpoint) pl ctx)
               fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
-  end;
+    None
+  end in
   (* Declare notations *)
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+  pstate
 
-let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+  let pstate =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -300,8 +305,8 @@ let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fixi
       Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
     let evd = Evd.from_ctx ctx in
-      Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
-      evd pl (Some(true,[],init_tac)) thms None
+    Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint)
+            evd pl (Some(true,[],init_tac)) thms None)
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -314,13 +319,15 @@ let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fixi
     let evd = Evd.restrict_universe_context evd vars in
     let ctx = Evd.check_univ_decl ~poly evd pl in
     let pl = Evd.universe_binders evd in
-    ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
+    ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, CoFixpoint) pl ctx)
               fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
-    cofixpoint_message fixnames
-  end;
+    cofixpoint_message fixnames;
+    None
+  end in
   (* Declare notations *)
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+  pstate
 
 let extract_decreasing_argument limit = function
   | (na,CStructRec) -> na
@@ -348,16 +355,18 @@ let check_safe () =
   let flags = Environ.typing_flags (Global.env ()) in
   flags.check_universes && flags.check_guarded
 
-let do_fixpoint local poly l =
+let do_fixpoint ~ontop local poly l =
   let fixl, ntns = extract_fixpoint_components true l in
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
   let possible_indexes =
     List.map compute_possible_guardness_evidences info in
-  declare_fixpoint local poly fix possible_indexes ntns;
-  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+  let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in
+  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
+  pstate
 
-let do_cofixpoint local poly l =
+let do_cofixpoint ~ontop local poly l =
   let fixl,ntns = extract_cofixpoint_components l in
   let cofix = interp_fixpoint ~cofix:true fixl ntns in
-  declare_cofixpoint local poly cofix ntns;
-  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+  let pstate = declare_cofixpoint ~ontop local poly cofix ntns in
+  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
+  pstate