diff options
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 7b63099c7..8c43888fb 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -25,6 +25,7 @@ open Tacexpr open Termops open Rawterm open Genarg +open Ind_tables (*i*) type orientation = bool @@ -137,3 +138,5 @@ val subst_all : ?strict:bool -> tactic (according to [dir] if given to get the rewrite direction) in the clause [cl] *) val replace_multi_term : bool option -> constr -> clause -> tactic + +val set_eq_dec_scheme_kind : mutual scheme_kind -> unit |