Imported Upstream version 8.3.pl2upstream/8.3.pl2

3 files changed, 16 insertions, 12 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index cf83c72a..3fc18219 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -10,7 +10,7 @@
  * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
  *)
 
-(* $Id: prettyp.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
+(* $Id: prettyp.ml 13967 2011-04-08 14:08:43Z herbelin $ *)
 
 open Pp
 open Util
@@ -460,13 +460,15 @@ let gallina_print_constant_with_infos sp =
   with_line_skip (print_name_infos (ConstRef sp))
 
 let gallina_print_syntactic_def kn =
-  let sep = " := "
-  and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
+  let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
   and (vars,a) = Syntax_def.search_syntactic_definition kn in
   let c = Topconstr.rawconstr_of_aconstr dummy_loc a in
-  str "Notation " ++ pr_qualid qid ++
-  prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++
-  Constrextern.without_symbols pr_lrawconstr c ++ fnl ()
+  hov 2
+    (hov 4
+       (str "Notation " ++ pr_qualid qid ++
+        prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++ 
+        spc () ++ str ":=") ++
+     spc () ++ Constrextern.without_symbols pr_rawconstr c) ++ fnl ()
 
 let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : "
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index f067fcf3..39477b0b 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: tacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: tacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *)
 
 open Util
 open Genarg
@@ -55,7 +55,7 @@ let rec make_let e = function
 let add_clause s (pt,e) l =
   let p = make_patt pt in
   let w = Some (make_when (MLast.loc_of_expr e) pt) in
-  (p, w, make_let e pt)::l
+  (p, <:vala< w >>, make_let e pt)::l
 
 let rec extract_signature = function
   | [] -> []
@@ -72,7 +72,8 @@ let check_unicity s l =
 let make_clauses s l =
   check_unicity s l;
   let default =
-    (<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in
+    (<:patt< _ >>,<:vala<None>>,
+     <:expr< failwith "Tactic extension: cannot occur" >>) in
   List.fold_right (add_clause s) l [default]
 
 let rec make_args = function
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 95eccfda..860110e5 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: vernacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: vernacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *)
 
 open Util
 open Genarg
@@ -31,7 +31,7 @@ let rec make_let e = function
 let add_clause s (_,pt,e) l =
   let p = make_patt pt in
   let w = Some (make_when (MLast.loc_of_expr e) pt) in
-  (p, w, make_let e pt)::l
+  (p, <:vala<w>>, make_let e pt)::l
 
 let check_unicity s l =
   let l' = List.map (fun (_,l,_) -> extract_signature l) l in
@@ -43,7 +43,8 @@ let check_unicity s l =
 let make_clauses s l =
   check_unicity s l;
   let default =
-    (<:patt< _ >>,None,<:expr< failwith "Vernac extension: cannot occur" >>) in
+    (<:patt< _ >>,<:vala<None>>,
+     <:expr< failwith "Vernac extension: cannot occur" >>) in
   List.fold_right (add_clause s) l [default]
 
 let mlexpr_of_clause =