diff options
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index cab7a15d2..0a44a9553 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,2 +1,22 @@ (* $Id$ *) + +(*i*) +open Term +open Sign +open Environ +open Reduction +open Evarutil +(*i*) + +val reset_problems : unit -> unit +val the_conv_x : unsafe_env -> 'a evar_defs -> constr -> constr -> bool +val the_conv_x_leq : unsafe_env -> 'a evar_defs -> constr -> constr -> bool + + +(* For debugging *) +val solve_pb : 'c evar_defs -> conv_pb * constr * constr -> bool +val evar_conv_x : 'c evar_defs -> context option -> + conv_pb -> constr -> constr -> bool +val evar_eqappr_x : 'c evar_defs -> context option -> + conv_pb -> constr * constr list -> constr * constr list -> bool |