diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-10 00:37:49 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-10 00:37:49 +0000 |
| commit | 910612984259c0c032f1292ce4d7ac6f290b8e20 (patch) | |
| tree | 308624ce73c8a8469a6fa0640d06ed055c643adc /pretyping/pretype_errors.mli | |
| parent | 8a590a18d267424809c9bbea5017e0d9e993c663 (diff) | |
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
Diffstat (limited to 'pretyping/pretype_errors.mli')
| -rw-r--r-- | pretyping/pretype_errors.mli | 14 |
1 files changed, 0 insertions, 14 deletions
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 |