diff options
| author | herbelin | 2010-07-22 21:06:06 +0000 |
|---|---|---|
| committer | herbelin | 2010-07-22 21:06:06 +0000 |
| commit | 9b4927d7fdbbafa7ed372e152e7106b3055dfb99 (patch) | |
| tree | c395758164096f2a33ae8d57d2a2895cfa3203b8 /toplevel | |
| parent | 53b06c3069c1234368d14de64ddd9382ff705f3b (diff) | |
Constrintern: unified push_name_env and push_loc_name_env; made
location dumping for binders uniformly treated in constrintern.ml (and
renamed the optional arg of interp_context from fail_anonymous to
global_level since the flag now also decides whether to dump binders as
global or local ones); added locations for the variables occurring in
the "as in" clauses;
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13314 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 5 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
3 files changed, 3 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 3fa83662b2..a16afa86ce 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -67,8 +67,7 @@ let red_constant_entry n ce = function let interp_definition boxed bl red_option c ctypopt = let env = Global.env() in let evdref = ref Evd.empty in - let (env_bl, ctx), imps1 = - interp_context_evars ~fail_anonymous:false evdref env bl in + let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in let imps,ce = match ctypopt with None -> @@ -225,7 +224,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = let env0 = Global.env() in let evdref = ref Evd.empty in let (env_params, ctx_params), userimpls = - interp_context_evars ~fail_anonymous:false evdref env0 paramsl + interp_context_evars evdref env0 paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in diff --git a/toplevel/record.ml b/toplevel/record.ml index 89bf769114..12843da60d 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -60,7 +60,7 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields id t ps nots fs = let env0 = Global.env () in let evars = ref Evd.empty in - let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in + let (env1,newps), imps = interp_context_evars evars env0 ps in let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in let env2,impls,newfs,data = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0ed1186a05..6a1eff333c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -599,7 +599,6 @@ let vernac_instance abst glob sup inst props pri = ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri) let vernac_context l = - List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l; Classes.context l let vernac_declare_instance glob id = |