Merge branch 'trunk' into pr379

6 files changed, 26 insertions, 28 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7eeb81050e..8fee191aff 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1591,7 +1591,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let idl_tmp = Array.map
           (fun ((loc,id),bl,ty,_) ->
             let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
-            let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbl in
+            let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> 
+                      Loc.raise ~loc (Stream.Error "pattern with quote not allowed after cofix")) rbl in
             (List.rev rbl,
              intern_type env' ty,env')) dl in
 	let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') ->
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index b020f89457..9f549b0c0f 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -173,32 +173,33 @@ let cook_notation df sc =
   (* - all single quotes in terminal tokens are doubled                       *)
   (* - characters < 32 are represented by '^A, '^B, '^C, etc                  *)
   (* The output is decoded in function Index.prepare_entry of coqdoc          *)
-  let ntn = String.make (String.length df * 5) '_' in
+  let ntn = Bytes.make (String.length df * 5) '_' in
   let j = ref 0 in
   let l = String.length df - 1 in
   let i = ref 0 in
+  let open Bytes in             (* Bytes.set *)
   while !i <= l do
     assert (df.[!i] != ' ');
     if df.[!i] == '_' && (Int.equal !i l || df.[!i+1] == ' ') then
       (* Next token is a non-terminal *)
-      (ntn.[!j] <- 'x'; incr j; incr i)
+      (set ntn !j 'x'; incr j; incr i)
     else begin
       (* Next token is a terminal *)
-      ntn.[!j] <- '\''; incr j;
+      set ntn !j '\''; incr j;
       while !i <= l && df.[!i] != ' ' do
 	if df.[!i] < ' ' then
 	  let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in
 	  (String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i)
 	else begin
-	  if df.[!i] == '\'' then (ntn.[!j] <- '\''; incr j);
-	  ntn.[!j] <- df.[!i]; incr j; incr i
+	  if df.[!i] == '\'' then (set ntn !j '\''; incr j);
+	  set ntn !j df.[!i]; incr j; incr i
 	end
       done;
-      ntn.[!j] <- '\''; incr j
+      set ntn !j '\''; incr j
     end;
-    if !i <= l then (ntn.[!j] <- '_'; incr j; incr i)
+    if !i <= l then (set ntn !j '_'; incr j; incr i)
   done;
-  let df = String.sub ntn 0 !j in
+  let df = Bytes.sub_string ntn 0 !j in
   match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
 
 let dump_notation_location posl df (((path,secpath),_),sc) =
diff --git a/interp/notation.ml b/interp/notation.ml
index 29e5a3bfd8..90ac7f7296 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -927,19 +927,19 @@ let locate_notation prglob ntn scope =
   match ntns with
   | [] -> str "Unknown notation"
   | _ ->
-    t (str "Notation            " ++
-    tab () ++ str "Scope     " ++ tab () ++ fnl () ++
+    str "Notation" ++ fnl () ++
     prlist (fun (ntn,l) ->
       let scope = find_default ntn scopes in
       prlist
 	(fun (sc,r,(_,df)) ->
 	  hov 0 (
-	    pr_notation_info prglob df r ++ tbrk (1,2) ++
-	    (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++
-	    tbrk (1,2) ++
-	    (if Option.equal String.equal (Some sc) scope then str "(default interpretation)" else mt ())
+	    pr_notation_info prglob df r ++
+	    (if String.equal sc default_scope then mt ()
+             else (spc () ++ str ": " ++ str sc)) ++
+	    (if Option.equal String.equal (Some sc) scope
+             then spc () ++ str "(default interpretation)" else mt ())
 	    ++ fnl ()))
-	l) ntns)
+	l) ntns
 
 let collect_notation_in_scope scope sc known =
   assert (not (String.equal scope default_scope));
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 37bbe0ce87..87ca253253 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -23,12 +23,9 @@ type ppbox =
   | PpHOVB of int
   | PpHVB of int
   | PpVB of int
-  | PpTB
 
 type ppcut =
   | PpBrk of int * int
-  | PpTbrk of int * int
-  | PpTab
   | PpFnl
 
 let ppcmd_of_box = function
@@ -36,13 +33,10 @@ let ppcmd_of_box = function
   | PpHOVB n -> hov n
   | PpHVB n -> hv n
   | PpVB n -> v n
-  | PpTB   -> t
 
 let ppcmd_of_cut = function
-  | PpTab -> tab ()
   | PpFnl -> fnl ()
   | PpBrk(n1,n2) -> brk(n1,n2)
-  | PpTbrk(n1,n2) -> tbrk(n1,n2)
 
 type unparsing =
   | UnpMetaVar of int * parenRelation
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index de7a42eee5..09dc369437 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -23,12 +23,9 @@ type ppbox =
   | PpHOVB of int
   | PpHVB of int
   | PpVB of int
-  | PpTB
 
 type ppcut =
   | PpBrk of int * int
-  | PpTbrk of int * int
-  | PpTab
   | PpFnl
 
 val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 407cec0842..fd57b70ca9 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -60,6 +60,9 @@ let rec cases_pattern_fold_names f a = function
   | CPatPrim _ | CPatAtom _ -> a
   | CPatCast _ -> assert false
 
+let ids_of_pattern =
+  cases_pattern_fold_names Id.Set.add Id.Set.empty
+
 let ids_of_pattern_list =
   List.fold_left
     (Loc.located_fold_left
@@ -173,7 +176,8 @@ let split_at_annot bl na =
               (List.rev ans, LocalRawAssum (r, k, t) :: rest)
             end
 	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
-        | LocalPattern _ :: rest -> assert false
+        | LocalPattern (loc,_,_) :: rest ->
+            Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
             user_err ~loc 
 			 (str "No parameter named " ++ Nameops.pr_id id ++ str".")
@@ -196,8 +200,9 @@ let map_local_binders f g e bl =
         (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl)
     | LocalRawDef((loc,na),ty) ->
         (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl)
-    | LocalPattern _ ->
-        assert false in
+    | LocalPattern (loc,pat,t) ->
+        let ids = ids_of_pattern pat in
+        (Id.Set.fold g ids e, LocalPattern (loc,pat,Option.map (f e) t)::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)