diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-24 17:55:44 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-24 17:55:44 +0000 |
commit | 6e9f19b7dc30eb451dc4cb67be0dd202eab22718 (patch) | |
tree | 698a588326a04807b8e79057338db51625783447 /pretyping/evarconv.mli | |
parent | c2e126d2a753e57a3ec0b65760655dc08d79e2b2 (diff) |
Versions initiales
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@136 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |