diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-01 08:20:00 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-01 08:20:00 +0000 |
| commit | b91ae6a8900b368af0a3acc0a61a8af0db783991 (patch) | |
| tree | 83655138d0dfc193b046f34c63150ff9d187b9e4 /pretyping/evarconv.mli | |
| parent | dda7c7bb0b6ea0c2106459d8ae208eff0dfd6738 (diff) | |
- environment -> safe_environment
- unsafe_env -> env
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@168 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 59dfc7895..9310e5dd3 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -11,18 +11,18 @@ open Evarutil val reset_problems : unit -> unit -val the_conv_x : unsafe_env -> unit evar_defs -> constr -> constr -> bool +val the_conv_x : env -> unit evar_defs -> constr -> constr -> bool -val the_conv_x_leq : unsafe_env -> unit evar_defs -> constr -> constr -> bool +val the_conv_x_leq : env -> unit evar_defs -> constr -> constr -> bool (* For debugging *) val solve_pb : - unsafe_env -> unit evar_defs -> conv_pb * constr * constr -> bool + env -> unit evar_defs -> conv_pb * constr * constr -> bool val evar_conv_x : - unsafe_env -> unit evar_defs -> + env -> unit evar_defs -> conv_pb -> constr -> constr -> bool val evar_eqappr_x : - unsafe_env -> unit evar_defs -> + env -> unit evar_defs -> conv_pb -> constr * constr list -> constr * constr list -> bool |