diff options
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 162698112..3f67924c7 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -56,9 +56,6 @@ type 'a clausenv = { type wc = named_context sigma (* for a better reading of the following *) val unify : constr -> tactic -val unify_0 : - Reductionops.conv_pb -> wc -> constr -> constr - -> (int * constr) list * (constr * constr) list val collect_metas : constr -> int list val mk_clenv : 'a -> constr -> 'a clausenv @@ -131,3 +128,7 @@ val pr_clenv : 'a clausenv -> Pp.std_ppcmds val abstract_list_all : Environ.env -> Evd.evar_map -> constr -> constr -> constr list -> constr +(* For debug *) +val unify_0 : + bool -> Reductionops.conv_pb -> wc -> constr -> constr + -> (int * constr) list * (constr * constr) list |