diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-07 19:28:25 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-07 19:28:25 +0000 |
| commit | d331f7f1ac0ec2ed12d458597d558a1988db1ba6 (patch) | |
| tree | 0e5addad213aeb1d647a0411285754e8a9cb23f6 /pretyping/evarconv.mli | |
| parent | 11104cdcb1e53cd83768d2ce9858829b457e2d65 (diff) | |
deuxieme vague de modifs: evar_defs fonctionnel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index c8b234ee2..5deccaa8b 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -16,13 +16,20 @@ open Reductionops open Evarutil (*i*) -val the_conv_x : env -> evar_defs -> constr -> constr -> bool +(* returns exception Reduction.NotConvertible if not unifiable *) +val the_conv_x : env -> constr -> constr -> evar_defs -> evar_defs +val the_conv_x_leq : env -> constr -> constr -> evar_defs -> evar_defs -val the_conv_x_leq : env -> evar_defs -> constr -> constr -> bool +(* The same function resolving evars by side-effect and + catching the exception *) +val e_conv : env -> evar_defs ref -> constr -> constr -> bool +val e_cumul : env -> evar_defs ref -> constr -> constr -> bool (*i For debugging *) -val evar_conv_x : env -> evar_defs -> conv_pb -> constr -> constr -> bool +val evar_conv_x : + env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool val evar_eqappr_x : env -> evar_defs -> - conv_pb -> constr * constr list -> constr * constr list -> bool + conv_pb -> constr * constr list -> constr * constr list -> + evar_defs * bool (*i*) |