diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-16 19:15:17 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-16 19:15:17 +0000 |
| commit | 571c03b533cfbeabe9140534604feb7cb8a4e5f1 (patch) | |
| tree | 212a9c005fec551693c2b84c78428e3a4c93bf60 /toplevel/command.ml | |
| parent | 96557853c935486137379ad19fd2dbc206ea74a8 (diff) | |
(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record); args scope dans Declare
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4401 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index acad66057..78d208437 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -256,6 +256,10 @@ let interp_mutual lparams lnamearconstrs finite = let env_params, params = List.fold_left (fun (env, params) d -> match d with + | LocalRawAssum ([_,na],(CHole _ as t)) -> + let t = interp_binder sigma env na t in + let d = (na,None,t) in + (push_rel d env, d::params) | LocalRawAssum (nal,t) -> let t = interp_type sigma env t in let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in @@ -394,11 +398,6 @@ let build_mutual lind finite = option_iter (fun (_,names,(df,scope)) -> Metasyntax.add_notation_interpretation df (ARef (IndRef (kn,i)),names) scope)) notations; - list_iter_i (fun i (_,_,_,_,lc) -> - Symbols.declare_ref_arguments_scope (IndRef (kn,i)); - for j=1 to List.length lc do - Symbols.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); - done) lind; List.iter (fun id -> Class.try_add_new_coercion (locate (make_short_qualid id)) Global) coes |