diff options
| -rw-r--r-- | tactics/rewrite.ml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 6d26e91c6..b442ca98b 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -631,13 +631,19 @@ let poly_inverse sort = type rewrite_proof = | RewPrf of constr * constr + (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *) | RewCast of cast_kind + (** A proof of convertibility (with casts) *) type rewrite_result_info = { rew_car : constr; + (** A type *) rew_from : constr; + (** A term of type rew_car *) rew_to : constr; + (** A term of type rew_car *) rew_prf : rewrite_proof; + (** A proof of rew_from == rew_to *) rew_evars : evars; } @@ -646,9 +652,14 @@ type rewrite_result = | Identity | Success of rewrite_result_info -type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types -> - (bool (* prop *) * constr option) -> evars -> - 'a * rewrite_result +type 'a pure_strategy = + 'a -> (* a parameter: for instance, a state *) + Environ.env -> + Id.t list -> (* Unfresh names *) + constr -> types -> (* first term and its type (convertible to rew_from) *) + (bool (* prop *) * constr option) -> + evars -> + 'a * rewrite_result (* the updated state for instance and the "result" *) type strategy = unit pure_strategy |