From 9b4927d7fdbbafa7ed372e152e7106b3055dfb99 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Jul 2010 21:06:06 +0000
Subject: 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
---
 toplevel/command.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'toplevel/command.ml')

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
 
-- 
cgit v1.2.3