diff options
| author | herbelin | 2000-09-10 07:19:28 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-10 07:19:28 +0000 |
| commit | 79dc33cbc403ebab0bd1fe815c13f740f0a1b850 (patch) | |
| tree | e38e167003d7dd97d95a59ea7c026a1629b346f8 /kernel/safe_typing.ml | |
| parent | c0ff579606f2eba24bc834316d8bb7bcc076000d (diff) | |
Ajout d'un LetIn primitif.
Abstraction de constr via kind_of_constr dans une bonne partie du code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ca5d4a2ecc..6b97c63ac6 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -5,7 +5,7 @@ open Pp open Util open Names open Univ -open Generic +(*i open Generic i*) open Term open Reduction open Sign @@ -122,6 +122,16 @@ let rec execute mf env cstr = let (j,cst3) = gen_rel env1 Evd.empty name varj j' in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (j, cst) + + | IsLetIn (name,c1,c2,c3) -> + let (j1,cst1) = execute mf env c1 in + let (j2,cst2) = execute mf env c2 in + let { uj_val = b; uj_type = t } = cast_rel env Evd.empty j1 j2 in + let (j3,cst3) = execute mf (push_rel_def (name,b,t) env) c3 in + let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in + ({ uj_val = mkLetIn (name, j1.uj_val, j2.uj_val, j3.uj_val) ; + uj_type = typed_app (subst1 j1.uj_val) j3.uj_type }, + cst) | IsCast (c,t) -> let (cj,cst1) = execute mf env c in |