diff options
| author | Gaëtan Gilbert | 2019-05-03 14:14:40 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | b8842c3c8d6e6d9d4c19a75453fca9f94de6fa49 (patch) | |
| tree | 9c52ce44b68ecc40dfe6805adb559d2ff110032f /plugins/ltac/rewrite.mli | |
| parent | 8abacf00c6c39ec98085d531737d18edc9c19b2a (diff) | |
coqpp: add new ![] specifiers for structured proof interaction
![proof_stack] is equivalent to the old meaning of ![proof]: the body
has type `pstate:Proof_global.t option -> Proof_global.t option`
The other specifiers are for the following body types:
~~~
![open_proof] `is_ontop:bool -> pstate`
![maybe_open_proof] `is_ontop:bool -> pstate option`
![proof] `pstate:pstate -> pstate`
![proof_opt_query] `pstate:pstate option -> unit`
![proof_query] `pstate:pstate -> unit`
~~~
The `is_ontop` is only used for the warning message when declaring a
section variable inside a proof, we could also just stop warning.
The specifiers look closely related to stm classifiers, but currently
they're unconnected. Notably this means that a ![proof_query] doesn't
have to be classified QUERY.
![proof_stack] is only used by g_rewrite/rewrite whose behaviour I
don't fully understand, maybe we can drop it in the future.
For compat we may want to consider keeping ![proof] with its old
meaning and using some new name for the new meaning. OTOH fixing
plugins to be stricter is easier if we change it as the errors tell us
where it's used.
Diffstat (limited to 'plugins/ltac/rewrite.mli')
| -rw-r--r-- | plugins/ltac/rewrite.mli | 35 |
1 files changed, 26 insertions, 9 deletions
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index cab7d0065e..e1cbc46b3b 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -81,18 +81,35 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : pstate:Proof_global.t option -> rewrite_attributes -> - ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> - constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option - -val add_setoid : pstate:Proof_global.t option -> - rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> - Id.t -> Proof_global.t option +val declare_relation + : rewrite_attributes + -> ?binders:local_binder_expr list + -> constr_expr + -> constr_expr + -> Id.t + -> constr_expr option + -> constr_expr option + -> constr_expr option + -> unit + +val add_setoid + : rewrite_attributes + -> local_binder_expr list + -> constr_expr + -> constr_expr + -> constr_expr + -> Id.t + -> unit val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option -val add_morphism : pstate:Proof_global.t option -> - rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option +val add_morphism + : rewrite_attributes + -> local_binder_expr list + -> constr_expr + -> constr_expr + -> Id.t + -> Proof_global.pstate val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr |