diff options
| author | filliatr | 1999-11-29 14:29:18 +0000 |
|---|---|---|
| committer | filliatr | 1999-11-29 14:29:18 +0000 |
| commit | 958b0daa566c3735e054eb76d05255101ef29851 (patch) | |
| tree | 083f3fc4e78e4cbd5ce18539cc3c574276a04118 /proofs | |
| parent | c4aad6897210f9e55cb41a9dd40fc1fd01321f6b (diff) | |
portage modules Evarconv et Evarutil
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@161 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/typing_ev.ml | 6 | ||||
| -rw-r--r-- | proofs/typing_ev.mli | 3 |
2 files changed, 8 insertions, 1 deletions
diff --git a/proofs/typing_ev.ml b/proofs/typing_ev.ml index 5e48153719..741ef10409 100644 --- a/proofs/typing_ev.ml +++ b/proofs/typing_ev.ml @@ -146,5 +146,9 @@ let type_of env sigma c = (* The typed type of a judgment. *) let execute_type env sigma constr = - let j = safe_machine env sigma constr in + let j = execute { fix=false; nocheck=true } env sigma constr in + assumption_of_judgment env sigma j + +let execute_type env sigma constr = + let j = execute { fix=false; nocheck=false } env sigma constr in assumption_of_judgment env sigma j diff --git a/proofs/typing_ev.mli b/proofs/typing_ev.mli index f24ee3914a..b12cd369d3 100644 --- a/proofs/typing_ev.mli +++ b/proofs/typing_ev.mli @@ -13,3 +13,6 @@ open Evd val type_of : unsafe_env -> 'a evar_map -> constr -> constr val execute_type : unsafe_env -> 'a evar_map -> constr -> typed_type + +val execute_rec_type : unsafe_env -> 'a evar_map -> constr -> typed_type + |