diff options
| author | Gaëtan Gilbert | 2019-05-02 19:46:02 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 8abacf00c6c39ec98085d531737d18edc9c19b2a (patch) | |
| tree | 52127cb4b3909e94e53996cd9e170de1f2ea6726 /vernac/comFixpoint.ml | |
| parent | 1c228b648cb1755cad3ec1f38690110d6fe14bc5 (diff) | |
Proof_global: pass only 1 pstate when we don't want the proof stack
Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.
Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).
We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.
Behaviour should be similar modulo bugs, let's see what CI says.
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a428c42e49..006ac314a5 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -255,7 +255,7 @@ let interp_fixpoint ~cofix l ntns = let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) -let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = +let declare_fixpoint 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 *) @@ -267,7 +267,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx fixdefs) in let evd = Evd.from_ctx ctx in Some - (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint) + (Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint) evd pl (Some(false,indexes,init_tac)) thms None) else begin (* We shortcut the proof process *) @@ -294,7 +294,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; pstate -let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = +let declare_cofixpoint 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 *) @@ -305,7 +305,7 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in - Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint) + Some (Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) evd pl (Some(true,[],init_tac)) thms None) else begin (* We shortcut the proof process *) @@ -366,18 +366,18 @@ let check_safe () = let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded -let do_fixpoint ~ontop local poly l = +let do_fixpoint local poly l = let fixl, ntns = extract_fixpoint_components ~structonly: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 - let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in + let pstate = declare_fixpoint local poly fix possible_indexes ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); pstate -let do_cofixpoint ~ontop local poly l = +let do_cofixpoint local poly l = let fixl,ntns = extract_cofixpoint_components l in let cofix = interp_fixpoint ~cofix:true fixl ntns in - let pstate = declare_cofixpoint ~ontop local poly cofix ntns in + let pstate = declare_cofixpoint local poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); pstate |