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.mli | |
| 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.mli')
| -rw-r--r-- | vernac/comFixpoint.mli | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 5937842f17..d36593332e 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -19,14 +19,12 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : - ontop:Proof_global.t option -> (* When [false], assume guarded. *) - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t option + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.pstate option val do_cofixpoint : - ontop:Proof_global.t option -> (* When [false], assume guarded. *) - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t option + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.pstate option (************************************************************************) (** Internal API *) @@ -83,20 +81,18 @@ val interp_fixpoint : (** [Not used so far] *) val declare_fixpoint : - ontop:Proof_global.t option -> locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * (Constr.rel_context * Impargs.manual_implicits * int option) list -> Proof_global.lemma_possible_guards -> decl_notation list -> - Proof_global.t option + Proof_global.pstate option val declare_cofixpoint : - ontop:Proof_global.t option -> locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * (Constr.rel_context * Impargs.manual_implicits * int option) list -> decl_notation list -> - Proof_global.t option + Proof_global.pstate option (** Very private function, do not use *) val compute_possible_guardness_evidences : |