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
---
 interp/constrextern.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 28cd12fbde..95a669f751 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -684,10 +684,10 @@ let rec extern inctx scopes vars r =
         let na' = match na,tm with
             Anonymous, RVar (_,id) when
               rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
-              -> Some Anonymous
+              -> Some (dummy_loc,Anonymous)
           | Anonymous, _ -> None
           | Name id, RVar (_,id') when id=id' -> None
-          | Name _, _ -> Some na in
+          | Name _, _ -> Some (dummy_loc,na) in
 	(sub_extern false scopes vars tm,
 	(na',Option.map (fun (loc,ind,n,nal) ->
 	  let params = list_tabulate
@@ -701,15 +701,15 @@ let rec extern inctx scopes vars r =
       CCases (loc,sty,rtntypopt',tml,eqns)
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
-      CLetTuple (loc,nal,
-        (Option.map (fun _ -> na) typopt,
+      CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal,
+        (Option.map (fun _ -> (dummy_loc,na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern inctx scopes (List.fold_left add_vname vars nal) b)
 
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
-        (Option.map (fun _ -> na) typopt,
+        (Option.map (fun _ -> (dummy_loc,na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
 
-- 
cgit v1.2.3