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/command.ml | |
| 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/command.ml')
| -rw-r--r-- | toplevel/command.ml | 5 |
1 files changed, 2 insertions, 3 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 |