diff options
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8b41b9c9b5..738a951470 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -114,6 +114,8 @@ sig val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment + val check_evars : env -> evar_map -> evar_defs ref -> constr -> unit + (*i*) (* Internal of Pretyping... * Unused outside, but useful for debugging diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index ca1a1ded4c..06b290b1da 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -78,6 +78,7 @@ sig (* Idem but do not fail on unresolved evars *) val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment + val check_evars : env -> evar_map -> evar_defs ref -> constr -> unit (*i*) (* Internal of Pretyping... |