Imported Upstream version 8.3pl1upstream/8.3pl1

3 files changed, 40 insertions, 20 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d918e94d..524448a6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
+(* $Id: constrintern.ml 13620 2010-11-04 14:11:49Z herbelin $ *)
 
 open Pp
 open Util
@@ -266,6 +266,9 @@ let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars =
   try
     let idscopes,typ = List.assoc id ntnvars in
     if !idscopes <> None &
+      (* scopes have no effect on the interpretation of identifiers, hence
+         we can tolerate having a variable occurring several times in
+         different scopes: *) typ <> NtnInternTypeIdent &
       make_current_scope (Option.get !idscopes)
       <> make_current_scope (scopt,scopes) then
 	error_inconsistent_scope loc id
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 0a42b78b..020c3622 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dumpglob.ml 13328 2010-07-26 11:05:30Z herbelin $ *)
+(* $Id: dumpglob.ml 13674 2010-12-04 10:34:11Z herbelin $ *)
 
 
 (* Dump of globalization (to be used by coqdoc) *)
@@ -181,15 +181,32 @@ let dump_libref loc dp ty =
 		  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
 
 let cook_notation df sc =
+  (* We encode notations so that they are space-free and still human-readable *)
+  (* - all spaces are replaced by _ *)
+  (* - all _ denoting a non-terminal symbol are replaced by x *)
+  (* - all terminal tokens are surrounded by single quotes, including '_' *)
+  (*   which already denotes terminal _ *)
+  (* - all single quotes in terminal tokens are doubled *)
+  (* The output is decoded in function Index.prepare_entry of coqdoc *)
   let ntn = String.make (String.length df * 3) '_' in
   let j = ref 0 in
-  let quoted = ref false in
-  for i = 0 to String.length df - 1 do
-    if df.[i] = '\'' then quoted := not !quoted;
-    if df.[i] = ' ' then (ntn.[!j] <- '_'; incr j) else
-    if df.[i] = '_' && not !quoted then (ntn.[!j] <- 'x'; incr j) else
-    if df.[i] = 'x' && not !quoted then (String.blit "'x'" 0 ntn !j 3; j := !j + 3) else
-    (ntn.[!j] <- df.[i]; incr j)
+  let l = String.length df - 1 in
+  let i = ref 0 in
+  while !i <= l do
+    assert (df.[!i] <> ' ');
+    if df.[!i] = '_' && (!i = l || df.[!i+1] = ' ') then
+      (* Next token is a non-terminal *)
+      (ntn.[!j] <- 'x'; incr j; incr i)
+    else begin
+      (* Next token is a terminal *)
+      ntn.[!j] <- '\''; incr j;
+      while !i <= l && df.[!i] <> ' ' do
+	if df.[!i] = '\'' then (ntn.[!j] <- '\''; incr j);
+	ntn.[!j] <- df.[!i]; incr j; incr i
+      done;
+      ntn.[!j] <- '\''; incr j
+    end;
+    if !i <= l then (ntn.[!j] <- '_'; incr j; incr i)
   done;
   let df = String.sub ntn 0 !j in
   match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index b8a90088..a358249f 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.ml 13357 2010-07-29 22:59:55Z herbelin $ *)
+(* $Id: topconstr.ml 13680 2010-12-04 15:06:06Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -115,11 +115,11 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let outerl = [(ldots_var,inner)] in
       subst_rawvars outerl it
   | ALambda (na,ty,c) ->
-      let e,na = g e na in RLambda (loc,na,Explicit,f e ty,f e c)
+      let e',na = g e na in RLambda (loc,na,Explicit,f e ty,f e' c)
   | AProd (na,ty,c) ->
-      let e,na = g e na in RProd (loc,na,Explicit,f e ty,f e c)
+      let e',na = g e na in RProd (loc,na,Explicit,f e ty,f e' c)
   | ALetIn (na,b,c) ->
-      let e,na = g e na in RLetIn (loc,na,f e b,f e c)
+      let e',na = g e na in RLetIn (loc,na,f e b,f e' c)
   | ACases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
@@ -137,18 +137,18 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
 	(loc,idl,patl,f e rhs)) eqnl in
       RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
-      let e,nal = list_fold_map g e nal in
-      let e,na = g e na in
-      RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c)
+      let e',nal = list_fold_map g e nal in
+      let e'',na = g e na in
+      RLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c)
   | AIf (c,(na,po),b1,b2) ->
-      let e,na = g e na in
-      RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
+      let e',na = g e na in
+      RIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
   | ARec (fk,idl,dll,tl,bl) ->
-      let e,idl = array_fold_map (to_id g) e idl in
       let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
 	  let e,na = g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
-      RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl)
+      let e',idl = array_fold_map (to_id g) e idl in
+      RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
   | ACast (c,k) -> RCast (loc,f e c,
 			  match k with
 			    | CastConv (k,t) -> CastConv (k,f e t)