From 910612984259c0c032f1292ce4d7ac6f290b8e20 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sun, 10 Feb 2013 00:37:49 +0000 Subject: Moved code from Pretype_error to Evarutil git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16194 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pretype_errors.mli | 14 -------------- 1 file changed, 14 deletions(-) (limited to 'pretyping/pretype_errors.mli') diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 558f3d5bb..3a4c6aad5 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -43,20 +43,6 @@ exception PretypeError of env * Evd.evar_map * pretype_error val precatchable_exception : exn -> bool -(** Presenting terms without solved evars *) -val nf_evar : Evd.evar_map -> constr -> constr -val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment -val jl_nf_evar : Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list -val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array -val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment - -val env_nf_evar : Evd.evar_map -> env -> env -val env_nf_betaiotaevar : Evd.evar_map -> env -> env - -val j_nf_betaiotaevar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment -val jv_nf_betaiotaevar : - Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array - (** Raising errors *) val error_actual_type_loc : Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b -- cgit v1.2.3