diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-29 11:15:34 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-29 11:15:34 +0000 |
commit | 71c2c283334a7759d81a4d73905b513e3ed749fb (patch) | |
tree | e526be26c9500b6da46b36e59c6c51aa6f66ed8a /pretyping/retyping.mli | |
parent | c103130e36fd216acfd38c66a73748401751fd93 (diff) |
Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_of
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@532 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/retyping.mli')
-rw-r--r-- | pretyping/retyping.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index dd0727b03..379a03956 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -20,5 +20,8 @@ val get_type_of : env -> 'a evar_map -> constr -> constr val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr val get_sort_of : env -> 'a evar_map -> constr -> sorts -(*Makes an unsafe judgment from a constr*) -val mk_unsafe_judgment:env->'a evar_map->constr ->unsafe_judgment;; +(* Makes an assumption from a constr *) +val get_assumption_of : env -> 'a evar_map -> constr -> typed_type + +(* Makes an unsafe judgment from a constr *) +val get_judgment_of : env -> 'a evar_map -> constr -> unsafe_judgment |