diff options
| author | herbelin | 2003-09-16 19:14:43 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-16 19:14:43 +0000 |
| commit | 96557853c935486137379ad19fd2dbc206ea74a8 (patch) | |
| tree | 1191f6573464925a8c3095c99bdd765db5bb6269 | |
| parent | bf1ff3f34c386d3f846b08d66db4178d4bc4152e (diff) | |
(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4400 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/record.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index a165f006d8..aab5bc337d 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -49,6 +49,10 @@ let typecheck_params_and_fields ps fs = let env1,newps = List.fold_left (fun (env,newps) d -> match d with + | LocalRawAssum ([_,na],(CHole _ as t)) -> + let t = interp_binder Evd.empty env na t in + let d = (na,None,t) in + (push_rel d env, d::newps) | LocalRawAssum (nal,t) -> let t = interp_type Evd.empty env t in let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in |