diff options
Diffstat (limited to 'ltac/rewrite.mli')
| -rw-r--r-- | ltac/rewrite.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli index 378359d51..10fec2032 100644 --- a/ltac/rewrite.mli +++ b/ltac/rewrite.mli @@ -8,8 +8,8 @@ open Names open Constr -open EConstr open Environ +open EConstr open Constrexpr open Tacexpr open Misctypes @@ -75,7 +75,7 @@ val cl_rewrite_clause : bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic val is_applied_rewrite_relation : - env -> evar_map -> Context.Rel.t -> constr -> types option + env -> evar_map -> rel_context -> constr -> types option val declare_relation : ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t -> |