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 /plugins/funind/indfun.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 'plugins/funind/indfun.mli')
| -rw-r--r-- | plugins/funind/indfun.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index acf85f539e..cf4ef23d1a 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,10 +5,10 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val do_generate_principle : pstate:Proof_global.t option -> +val do_generate_principle : bool -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Proof_global.t option + Proof_global.pstate option val functional_induction : bool -> @@ -17,4 +17,4 @@ val functional_induction : Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val make_graph : pstate:Proof_global.t option -> GlobRef.t -> Proof_global.t option +val make_graph : ontop:Proof_global.t option -> GlobRef.t -> Proof_global.t option |