*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7

22 files changed, 366 insertions, 141 deletions

diff --git a/lib/pp.ml4 b/lib/pp.ml4
index d13044c9a0..0e4b6b05e0 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -101,15 +101,25 @@ let pifb () = [< 'Ppcmd_print_if_broken >]
 let ws n = [< 'Ppcmd_white_space n >]
 
 (* derived commands *)
+let mt () = [< >]
 let spc () = [< 'Ppcmd_print_break (1,0) >]
 let cut () = [< 'Ppcmd_print_break (0,0) >]
 let align () = [< 'Ppcmd_print_break (0,0) >]
 let int n = str (string_of_int n)
 let real r = str (string_of_float r)
 let bool b = str (string_of_bool b)
-let qstring s = str ("\""^(String.escaped s)^"\"")
+
+let rec escape_string s =
+  let rec escape_at s i =
+    if i<0 then s
+    else if s.[i] == '\\' || s.[i] == '"' then
+      let s' = String.sub s 0 i^"\\"^String.sub s i (String.length s - i) in
+      escape_at s' (i-1)
+    else escape_at s (i-1) in
+  escape_at s (String.length s - 1)
+
+let qstring s = str ("\""^(escape_string s)^"\"")
 let qs = qstring
-let mt () = [< >]
 
 (* boxing commands *)
 let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index a1208f48c1..f1b8b55750 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -207,9 +207,16 @@ GEXTEND Gram
       | IDENT "outside"; l = LIST1 global -> SearchOutside l
       | -> SearchOutside [] ] ]
   ;
-END;
+END
 
 (* Grammar extensions *)
+
+(* automatic translation of levels *)
+let adapt_level n = n*10
+let map_modl = function
+  | SetItemLevel(ids,n) -> SetItemLevel(ids,adapt_level n)
+  | SetLevel n -> SetLevel(adapt_level n)
+  | m -> m
 	  
 GEXTEND Gram
   GLOBAL: syntax;
@@ -251,25 +258,24 @@ GEXTEND Gram
          p = global;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc];
-         v8 = OPT[IDENT "V8only";
-                  op8=OPT STRING;
-                  n8=OPT natural;
-                  mv8=OPT["("; l = LIST1 syntax_modifier SEP ","; ")" -> l] ->
-                    (op8,n8,mv8) ] ->
+         (op8,nv8,mv8) =
+              [IDENT "V8only";
+               op8=OPT STRING;
+               n8=OPT natural;
+               mv8=OPT["("; l = LIST1 syntax_modifier SEP ","; ")" -> l] ->
+                    (op8,n8,mv8)
+              | -> (None,None,None)] ->
            let (ai,ni,b) = Metasyntax.interp_infix_modifiers a n modl in
-           let v8 =
-             let (op8,nv8,mv8) =
-               match v8 with
-                   Some (op8,nv8,mv8) ->
-                     let op8 = match op8 with Some s -> s | _ -> op in
-                     let nv8 = match nv8 with Some n -> Some n
-                       | _ -> Util.option_app (( * ) 10) n in
-                     let mv8 = match mv8 with Some m -> m | _ -> modl in
-                     (op8,nv8,mv8)
-                 | None ->  (op,Util.option_app(( * ) 10) n, modl) in
-             let (a8,n8,_) =
-               Metasyntax.interp_infix_modifiers a nv8 mv8 in
-             Some(a8,n8,op8) in
+           let op8 = match op8 with Some s -> s | _ -> op in
+           let nv8 = match nv8 with
+               Some n -> Some n
+             | _ -> Util.option_app adapt_level n in
+           let mv8 = match mv8 with
+               Some m -> m
+             | _ -> List.map map_modl modl in
+           let (a8,n8,_) =
+             Metasyntax.interp_infix_modifiers a nv8 mv8 in
+           let v8 = Some(a8,n8,op8) in
            VernacInfix (ai,ni,op,p,b,v8,sc)
      | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = global;
 	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc)
@@ -278,14 +284,17 @@ GEXTEND Gram
      | IDENT "Notation"; s = STRING; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ];
-         v8 = OPT[IDENT "V8only";
-                  s8=OPT STRING;
-                  mv8=["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8
-                      | ->[] ] -> (s8,mv8) ] ->
-           let v8 = Util.option_app (fun (s8,mv8) ->
-             let s8 = match s8 with Some s -> s | _ -> s in
-             (s8,mv8)) v8 in
-           VernacNotation (s,c,modl,v8,sc)
+         (s8,mv8) =
+             [IDENT "V8only";
+              s8=OPT STRING;
+              mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] ->
+                (s8,mv8)
+             | -> (None,None)] ->
+               let s8 = match s8 with Some s -> s | _ -> s in
+               let mv8 = match mv8 with
+                   Some mv8 -> mv8
+                 | _ -> List.map map_modl modl in
+               VernacNotation (s,c,modl,Some(s8,mv8),sc)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index e88e971411..0b6e344a9b 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -188,17 +188,38 @@ GEXTEND Gram
   ;
   (* (co)-fixpoints *)
   rec_definition:
-    [ [ id = base_ident; bl = LIST1 binder_nodef; ":"; type_ = lconstr;
-        ":="; def = lconstr ->
-          let ni = List.length (List.flatten (List.map fst bl)) - 1 in
+    [ [ id = base_ident; bl = LIST1 binder_nodef;
+        annot = OPT rec_annotation; type_ = type_cstr; ":="; def = lconstr ->
+          let names = List.map snd (List.flatten (List.map fst bl)) in
+          let ni =
+            match annot with
+                Some id ->
+                  (try list_index (Name id) names - 1
+                  with Not_found ->  Util.user_err_loc
+                      (loc,"Fixpoint",
+                       Pp.str "No argument named " ++ Nameops.pr_id id))
+              | None -> 
+                  if List.length names > 1 then
+                    Util.user_err_loc
+                      (loc,"Fixpoint",
+                       Pp.str "the recursive argument needs to be specified");
+                  0 in
           let loc0 = fst (List.hd (fst (List.hd bl))) in
           let loc1 = join_loc loc0 (constr_loc type_) in
           let loc2 = join_loc loc0 (constr_loc def) in
 	  (id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
   ;
   corec_definition:
-    [ [ id = base_ident; ":"; c = lconstr; ":="; def = lconstr ->
-          (id,c,def) ] ]
+    [ [ id = base_ident; bl = LIST0 binder_nodef; c = type_cstr; ":=";
+        def = lconstr ->
+          (id,CProdN(loc,bl,c),CLambdaN(loc,bl,def)) ] ]
+  ;
+  rec_annotation:
+    [ [ "{"; "struct"; id=IDENT; "}" -> id_of_string id ] ]
+  ;
+  type_cstr:
+    [ [ ":"; c=lconstr -> c 
+      | -> CHole loc ] ]
   ;
   (* Inductive schemes *)
   scheme:
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 54d0c42c02..549b78a836 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -249,7 +249,7 @@ let rec comment bp = parser
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
   | [< '_ as z; s >] -> 
 	(match z with
-	| '\n' | '\t' -> add_comment (); add_comment_pp (fnl ())
+	| '\n' -> add_comment (); add_comment_pp (fnl ())
 	| _ -> add_string (String.make 1 z)); comment bp s 
 
 (* Parse a special token, using the [token_tree] *)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 8ea4a25c3d..77afa80410 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -27,6 +27,10 @@ type cases_pattern =
   | PatVar of loc * name
   | PatCstr of loc * constructor * cases_pattern list * name
 
+let pattern_loc = function
+    PatVar(loc,_) -> loc
+  | PatCstr(loc,_,_,_) -> loc
+
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type fix_kind = RFix of (int array * int) | RCoFix of int
@@ -83,6 +87,23 @@ type rawconstr =
    - boolean in POldCase means it is recursive
 i*)
 
+let loc = function
+  | RVar (loc,_) -> loc
+  | RApp (loc,_,_) -> loc
+  | RLambda (loc,_,_,_) -> loc
+  | RProd (loc,_,_,_) -> loc
+  | RLetIn (loc,_,_,_) -> loc
+  | RCases (loc,_,_,_) -> loc
+  | ROrderedCase (loc,_,_,_,_) -> loc
+  | RRec (loc,_,_,_,_) -> loc
+  | RCast (loc,_,_) -> loc
+  | RSort (loc,_) -> loc
+  | RHole (loc,_) -> loc
+  | RRef (loc,_) -> loc
+  | REvar (loc,_) -> loc
+  | RMeta (loc,_) -> loc
+  | RDynamic (loc,_) -> loc
+
 let map_rawconstr f = function
   | RVar (loc,id) -> RVar (loc,id)
   | RApp (loc,g,args) -> RApp (loc,f g, List.map f args)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 981cb23314..b5e408bb54 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -27,6 +27,8 @@ type cases_pattern =
   | PatVar of loc * name
   | PatCstr of loc * constructor * cases_pattern list * name
 
+val pattern_loc : cases_pattern -> loc
+
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type fix_kind = RFix of (int array * int) | RCoFix of int
@@ -84,6 +86,8 @@ type rawconstr =
    - option in PHole tell if the "?" was apparent or has been implicitely added
 i*)
 
+val loc : rawconstr -> loc
+
 val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
 
 (*
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index 3b40228861..7fd29d5956 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -17,8 +17,7 @@ Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1).
 
 Notation "~ x" := (not x) (at level 5, right associativity)
   V8only (at level 55, right associativity).
-Notation "x = y" := (eq ? x y) (at level 5, no associativity)
-  V8only (at level 50, no associativity).
+Notation "x = y" := (eq ? x y) (at level 5, no associativity).
 
 Infix RIGHTA 6 "/\\" and.
 Infix RIGHTA 7 "\\/" or.
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 520e1971ff..1de5502678 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -12,10 +12,8 @@ Require Logic_Type.
 
 (** Symbolic notations for things in [Logic_type.v] *)
 
-Notation "x == y"  := (eqT ? x y)       (at level 5, no associativity)
-  V8only (at level 50, no associativity).
-Notation "x === y" := (identityT ? x y) (at level 5, no associativity)
-  V8only (at level 50, no associativity).
+Notation "x == y"  := (eqT ? x y)       (at level 5, no associativity).
+Notation "x === y" := (identityT ? x y) (at level 5, no associativity).
 
 (* Order is important to give printing priority to fully typed ALL and EX *)
 
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
index 2f53ca9b2a..b223f371f5 100644
--- a/theories/Init/PeanoSyntax.v
+++ b/theories/Init/PeanoSyntax.v
@@ -25,11 +25,11 @@ Module nat_scope.
 (* Warning: this hides sum and prod and breaks sumor symbolic notation *)
 Open Scope nat_scope.
 
-Infix 4 "+" plus : nat_scope  V8only 40.
-Infix 3 "*" mult : nat_scope  V8only 30.
-Infix NONA 5 "<=" le : nat_scope V8only 50.
-Infix NONA 5 "<" lt : nat_scope V8only 50.
-Infix NONA 5 ">=" ge : nat_scope V8only 50.
-Infix NONA 5 ">" gt : nat_scope V8only 50.
+Infix 4 "+" plus : nat_scope V8only (left associativity).
+Infix 3 "*" mult : nat_scope V8only (left associativity).
+Infix NONA 5 "<=" le : nat_scope.
+Infix NONA 5 "<" lt : nat_scope.
+Infix NONA 5 ">=" ge : nat_scope.
+Infix NONA 5 ">" gt : nat_scope.
 
 End nat_scope.
diff --git a/theories/Num/EqParams.v b/theories/Num/EqParams.v
index f7fec9f92f..c8fd74fcbf 100644
--- a/theories/Num/EqParams.v
+++ b/theories/Num/EqParams.v
@@ -14,7 +14,7 @@ Require Export Params.
 
 Parameter eqN:N->N->Prop.  
 
-(*i Infix 6 "=" eqN. i*)
+(*i Infix 6 "=" eqN V8only 50. i*)
 
 Grammar constr constr1 :=
 eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
@@ -22,4 +22,4 @@ eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
 Syntax constr
   level 1:
     equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
-.
\ No newline at end of file
+.
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v
index 7787c1f039..55912fdda5 100644
--- a/theories/Num/NSyntax.v
+++ b/theories/Num/NSyntax.v
@@ -10,12 +10,12 @@
 
 Require Export Params.
 
-Infix 6 "<" lt.
-Infix 6 "<=" le.
-Infix 6 ">" gt.
-Infix 6 ">=" ge.
+Infix 6 "<" lt V8only 50.
+Infix 6 "<=" le V8only 50.
+Infix 6 ">" gt V8only 50.
+Infix 6 ">=" ge V8only 50.
 
-(*i Infix 7 "+" plus. i*)
+(*i Infix 7 "+" plus V8only 40. i*)
 
 Grammar constr lassoc_constr4 :=
   squash_sum
@@ -32,4 +32,4 @@ Grammar constr lassoc_constr4 :=
 Syntax constr
   level 4:
     sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
\ No newline at end of file
+.
diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v
index 9d310a0398..0e00294223 100644
--- a/theories/Num/NeqDef.v
+++ b/theories/Num/NeqDef.v
@@ -15,7 +15,7 @@ Require EqParams.
 Require EqAxioms.
 
 Definition neq : N -> N -> Prop := [x,y] ~(x=y).
-Infix 6 "<>" neq.
+Infix 6 "<>" neq V8only 50.
 
 (* Proofs of axioms *)
 Lemma eq_not_neq : (x,y:N)x=y->~(x<>y).
diff --git a/theories/Num/NeqParams.v b/theories/Num/NeqParams.v
index 4e651954f2..7f7a5139e4 100644
--- a/theories/Num/NeqParams.v
+++ b/theories/Num/NeqParams.v
@@ -15,7 +15,7 @@ Require Export Params.
 
 Parameter neq : N -> N -> Prop.
 
-Infix 6 "<>" neq.
+Infix 6 "<>" neq V8only 50.
 
 
 
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index c07302f3f4..09de5a8e89 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -400,8 +400,7 @@ Qed.
 
 (***********)
 Definition Rsqr:R->R:=[r:R]``r*r``.
-Notation "x ²" := (Rsqr x) (at level 2,left associativity)
-  V8only (at level 20, left associativity).
+Notation "x ²" := (Rsqr x) (at level 2,left associativity).
 
 (***********)
 Lemma Rsqr_O:(Rsqr ``0``)==``0``.
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 5d2ec7aa73..60befa9da9 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -204,14 +204,10 @@ Delimits Scope R_scope with R.
 (* Warning: this hides sum and prod and breaks sumor symbolic notation *)
 Open Scope R_scope.
 
-Infix "<=" Rle (at level 5, no associativity) : R_scope
-  V8only (at level 50, no associativity).
-Infix "<"  Rlt (at level 5, no associativity) : R_scope
-  V8only (at level 50, no associativity).
-Infix ">=" Rge (at level 5, no associativity) : R_scope
-  V8only (at level 50, no associativity).
-Infix ">" Rgt (at level 5, no associativity) : R_scope
-  V8only (at level 50, no associativity).
+Infix "<=" Rle (at level 5, no associativity) : R_scope.
+Infix "<"  Rlt (at level 5, no associativity) : R_scope.
+Infix ">=" Rge (at level 5, no associativity) : R_scope.
+Infix ">" Rgt (at level 5, no associativity) : R_scope.
 Infix "+" Rplus (at level 4) : R_scope
   V8only (at level 40, left associativity).
 Infix "-" Rminus (at level 4) : R_scope
@@ -237,8 +233,7 @@ Notation  "x  <  y  <  z"  := (Rlt x y)/\(Rlt y z)
 Notation  "x  <  y  <=  z" := (Rlt x y)/\(Rle y z)
   (at level 5, y at level 4) : R_scope
   V8only (at level 50, y at level 49, no associativity).
-Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope
-  V8only (at level 50).
+Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope.
 Notation "/ x" := (Rinv x) (at level 0): R_scope
   V8only (at level 30, left associativity).
 
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index 5a170b5e5f..4624850e90 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -91,8 +91,7 @@ Qed.
 
 Definition eq_Dom [D1,D2:R->Prop] : Prop := (included D1 D2)/\(included D2 D1).
 
-Infix "=_D" eq_Dom (at level 5, no associativity)
-  V8only (at level 50, no associativity).
+Infix "=_D" eq_Dom (at level 5, no associativity).
 
 Lemma open_set_P1 : (D:R->Prop) (open_set D) <-> D =_D (interior D).
 Intro; Split.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index aa09915835..65b4422a11 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -288,10 +288,8 @@ Syntax constr
       	 -> [ (ZEXPR $n1):E " %" [1 0] (ZEXPR $n2):L ]
 .
 ].
-Infix 3 "/" Zdiv : Z_scope
-  V8only 30.
-Infix 3 "mod" Zmod : Z_scope
-  V8only 30.
+Infix 3 "/" Zdiv : Z_scope.
+Infix 3 "mod" Zmod : Z_scope.
 
 (** Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *)
 
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index 3f1abc8d72..a0610b56d2 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -260,8 +260,7 @@ Notation  "x = y = z" := x=y/\y=z
   (at level 5, y at level 4) : Z_scope
   V8only (at level 50, y at level 49).
 
-Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope
-  V8only (at level 50, no associativity).
+Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope.
 (* Notation "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*)
 
 V7only[
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 8b73960be5..cb33104e41 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -1020,8 +1020,7 @@ Fixpoint times [x:positive] : positive -> positive:=
   | xH => y
   end.
 
-Infix LEFTA 3 "*" times : positive_scope
-  V8only 30.
+Infix LEFTA 3 "*" times : positive_scope.
 
 (** Correctness of multiplication on positive *)
 Theorem times_convert :
@@ -1066,8 +1065,7 @@ Definition Zmult := [x,y:Z]
              end
     end.
 
-Infix LEFTA 3 "*" Zmult : Z_scope
-  V8only 30.
+Infix LEFTA 3 "*" Zmult : Z_scope.
 
 Open Scope Z_scope.
 
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 14375e04ec..2d86e00c93 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -147,6 +147,9 @@ let pr_binder pr (nal,t) =
 let pr_binders pr bl =
   hv 0 (prlist_with_sep sep (pr_binder pr) bl)
 
+let pr_arg_binders pr bl =
+  if bl = [] then mt() else (spc() ++ pr_binders pr bl)
+
 let pr_global vars ref = pr_global_env vars ref
 
 let split_lambda = function
@@ -162,6 +165,158 @@ let split_product = function
   | CProdN (loc,(na::nal,t)::bl,c) -> (na,t,CProdN(loc,(nal,t)::bl,c))
   | _ -> anomaly "ill-formed fixpoint body"
 
+let rec extract_lam_binders c =
+  match c with
+      CLambdaN(loc,bl1,c') ->
+        let (bl,bd) = extract_lam_binders c' in
+        (bl1@bl, bd)
+    | _ -> ([],c)
+
+let rec extract_prod_binders c =
+  match c with
+      CProdN(loc,bl1,c') ->
+        let (bl,bd) = extract_prod_binders c' in
+        (bl1@bl, bd)
+    | _ -> ([],c)
+
+let rec check_same_pattern p1 p2 =
+  match p1, p2 with
+    | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when i1=i2 ->
+        check_same_pattern a1 a2
+    | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 ->
+        List.iter2 check_same_pattern a1 a2
+    | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> ()
+    | CPatNumeral(_,i1), CPatNumeral(_,i2) when i1=i2 -> ()
+    | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 ->
+        check_same_pattern e1 e2
+    | _ -> failwith "not same pattern"
+
+let check_same_ref r1 r2 =
+  match r1,r2 with
+  | Qualid(_,q1), Qualid(_,q2) when q1=q2 -> ()
+  | Ident(_,i1), Ident(_,i2) when i1=i2 -> ()
+  | _ -> failwith "not same ref"
+
+let rec check_same_type ty1 ty2 =
+  match ty1, ty2 with
+  | CRef r1, CRef r2 -> check_same_ref r1 r2
+  | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 ->
+      List.iter2 (fun (id1,i1,a1,b1) (id2,i2,a2,b2) ->
+        if id1<>id2 || i1<>i2 then failwith "not same fix";
+        check_same_type a1 a2;
+        check_same_type b1 b2)
+        fl1 fl2
+  | CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 ->
+      List.iter2 (fun (id1,a1,b1) (id2,a2,b2) ->
+        if id1<>id2 then failwith "not same fix";
+        check_same_type a1 a2;
+        check_same_type b1 b2)
+        fl1 fl2
+  | CArrow(_,a1,b1), CArrow(_,a2,b2) ->
+      check_same_type a1 a2;
+      check_same_type b1 b2
+  | CProdN(_,bl1,a1), CProdN(_,bl2,a2) ->
+      List.iter2 check_same_binder bl1 bl2;
+      check_same_type a1 a2
+  | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
+      List.iter2 check_same_binder bl1 bl2;
+      check_same_type a1 a2
+  | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 ->
+      check_same_type a1 a2;
+      check_same_type b1 b2
+  | CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 ->
+      List.iter2 check_same_type al1 al2
+  | CApp(_,e1,al1), CApp(_,e2,al2) ->
+      check_same_type e1 e2;
+      List.iter2 (fun (a1,e1) (a2,e2) ->
+                    if e1<>e2 then failwith "not same expl";
+                    check_same_type a1 a2) al1 al2
+  | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) ->
+      List.iter2 check_same_type a1 a2;
+      List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
+        List.iter2 check_same_pattern pl1 pl2;
+        check_same_type r1 r2) brl1 brl2
+  | COrderedCase(_,_,_,a1,bl1), COrderedCase(_,_,_,a2,bl2) ->
+      check_same_type a1 a2;
+      List.iter2 check_same_type bl1 bl2
+  | CHole _, CHole _ -> ()
+  | CMeta(_,i1), CMeta(_,i2) when i1=i2 -> ()
+  | CSort(_,s1), CSort(_,s2) when s1=s2 -> ()
+  | CCast(_,a1,b1), CCast(_,a2,b2) ->
+      check_same_type a1 a2;
+      check_same_type b1 b2
+  | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
+      List.iter2 check_same_type e1 e2
+  | CNumeral(_,i1), CNumeral(_,i2) when i1=i2 -> ()
+  | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
+      check_same_type e1 e2
+  | _ when ty1=ty2 -> ()
+  | _ -> failwith "not same type"
+
+and check_same_binder (nal1,e1) (nal2,e2) =
+  List.iter2 (fun (_,na1) (_,na2) ->
+    if na1<>na2 then failwith "not same name") nal1 nal2;
+  check_same_type e1 e2
+
+let merge_binders (na1,ty1) (na2,ty2) =
+  let na =
+    match snd na1, snd na2 with
+        Anonymous, Name id -> na2
+      | Name id, Anonymous -> na1
+      | Anonymous, Anonymous -> na1
+      | Name id1, Name id2 ->
+          if id1 <> id2 then failwith "not same name" else na1 in
+  let ty =
+    match ty1, ty2 with
+        CHole _, _ -> ty2
+      | _, CHole _ -> ty1
+      | _ ->
+          check_same_type ty1 ty2;
+          ty2 in
+  ([na],ty)
+            
+let rec strip_domain bvar c =
+  match c with
+    | CArrow(loc,a,b) ->
+        (merge_binders bvar ((dummy_loc,Anonymous),a), b)
+    | CProdN(loc,[([na],ty)],c') ->
+        (merge_binders bvar (na,ty), c')
+    | CProdN(loc,([na],ty)::bl,c') ->
+        (merge_binders bvar (na,ty), CProdN(loc,bl,c'))
+    | CProdN(loc,(na::nal,ty)::bl,c') ->
+        (merge_binders bvar (na,ty), CProdN(loc,(nal,ty)::bl,c'))
+    | _ -> failwith "not a product"
+
+(* Note: binder sharing is lost *)
+let rec strip_domains (nal,ty) c =
+  match nal with
+      [] -> assert false
+    | [na] ->
+        let bnd, c' = strip_domain (na,ty) c in
+        ([bnd],None,c')
+    | na::nal ->
+        let bnd, c1 = strip_domain (na,ty) c in
+        (try
+          let bl, rest, c2 = strip_domains (nal,ty) c1 in
+          (bnd::bl, rest, c2)
+        with Failure _ -> ([bnd],Some (nal,ty), c1))
+
+let rec extract_def_binders c ty =
+  match c with
+    | CLambdaN(loc,bvar::lams,b) ->
+        (try
+          let bvar', rest, ty' = strip_domains bvar ty in
+          let c' =
+            match rest, lams with
+                None,[] -> b
+              | None, _ -> CLambdaN(loc,lams,b)
+              | Some bvar,_ -> CLambdaN(loc,bvar::lams,b) in
+          let (bl,c2,ty2) = extract_def_binders c' ty' in
+          (bvar'@bl, c2, ty2)
+        with Failure _ ->
+          ([],c,ty))
+    | _ -> ([],c,ty)
+
 let rec split_fix n typ def =
   if n = 0 then ([],typ,def)
   else
@@ -174,8 +329,10 @@ let pr_recursive_decl pr id b t c =
   pr_id id ++ b ++ pr_opt_type_spc pr t ++ str " :=" ++
   brk(1,2) ++ pr ltop c
 
-let pr_fixdecl pr (id,n,t,c) =
-  let (bl,t,c) = split_fix (n+1) t c in
+let pr_fixdecl pr (id,n,t0,c0) =
+  let (bl,t,c) = extract_def_binders t0 c0 in
+  let (bl,t,c) =
+    if List.length bl <= n then split_fix (n+1) t0 c0 else (bl,t,c) in
   let annot =
     let ids = List.flatten (List.map fst bl) in
     if List.length ids > 1 then 
@@ -193,10 +350,6 @@ let pr_recursive pr_decl id = function
       prlist_with_sep (fun () -> fnl() ++ str "with ") pr_decl dl ++
       fnl() ++ str "for " ++ pr_id id
 
-let rec pr_arrow pr = function
-  | CArrow (_,a,b) -> pr (larrow,L) a ++ str " ->" ++ brk(1,0) ++ pr_arrow pr b
-  | a -> pr (-larrow,E) a
-
 let pr_annotation pr po =
   match po with
       None -> mt()
@@ -211,18 +364,24 @@ let rec pr inherited a =
   | CCoFix (_,id,cofix) ->
       hov 0 (str "cofix " ++ pr_recursive (pr_cofixdecl pr) (snd id) cofix),
       lfix
-  | CArrow _ -> hv 0 (pr_arrow pr a), larrow
-  | CProdN (_,bl,a) ->
-      hv 1 (
-	str "!" ++ pr_binders pr bl ++ str "." ++ spc()  ++ pr ltop a), lprod
-  | CLambdaN (_,bl,a) ->
+  | CArrow (_,a,b) ->
+      hov 0 (pr (larrow,L) a ++ str " ->" ++ brk(1,0) ++ pr (-larrow,E) b),
+      larrow
+  | CProdN _ ->
+      let (bl,a) = extract_prod_binders a in
+      hv 0 (str "!" ++ pr_binders pr bl ++ str "." ++ spc() ++ pr ltop a),
+      lprod
+  | CLambdaN _ ->
+      let (bl,a) = extract_lam_binders a in
       hov 2 (
 	str "fun" ++ spc () ++ pr_binders pr bl ++
         str " =>" ++ spc() ++ pr ltop a),
       llambda
   | CLetIn (_,x,a,b) ->
+      let (bl,a) = extract_lam_binders a in
       hv 0 (
-        hov 2 (str "let " ++ pr_name (snd x) ++ str " :=" ++ spc() ++
+        hov 2 (str "let " ++ pr_located pr_name x ++
+               pr_arg_binders pr bl ++ str " :=" ++ spc() ++
                pr ltop a ++ str " in") ++
         spc () ++ pr ltop b),
       lletin
@@ -285,18 +444,6 @@ let rec pr inherited a =
   if prec_less prec inherited then strm
   else str"(" ++ strm ++ str")"
 
-
-let rec fact_constr c =
-  match c with
-      CLambdaN(loc,bl1,CLambdaN(_,bl2,b)) ->
-        fact_constr (CLambdaN(loc,bl1@bl2,b))
-    | CProdN(loc,bl1,CProdN(_,bl2,b)) ->
-        fact_constr (CProdN(loc,bl1@bl2,b))
-    | _ -> map_constr_expr_with_binders
-        (fun _ -> fact_constr) (fun _ _ -> ()) () c
-let pr l c = pr l (fact_constr c)
-
-
 let transf env c =
   if Options.do_translate() then
     Constrextern.extern_rawconstr (Termops.vars_of_env env)
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 27e1307c59..fe1c560ca0 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -20,10 +20,18 @@ open Topconstr
 open Names
 open Util
 
-val prec_less : int -> int * Ppextend.parenRelation -> bool
+val extract_lam_binders :
+  constr_expr -> (name located list * constr_expr) list * constr_expr
+val extract_prod_binders :
+  constr_expr -> (name located list * constr_expr) list * constr_expr
+val extract_def_binders :
+  constr_expr -> constr_expr ->
+  (name located list * constr_expr) list *  constr_expr * constr_expr
+val split_fix :
+  int -> constr_expr -> constr_expr -> 
+  (name located list * constr_expr) list *  constr_expr * constr_expr
 
-val split_fix : int -> constr_expr -> constr_expr ->
-  (name located list * constr_expr) list * constr_expr * constr_expr
+val prec_less : int -> int * Ppextend.parenRelation -> bool
  
 val pr_global : Idset.t -> global_reference -> std_ppcmds
  
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 9a0bc64f8d..2ba13bb793 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -189,6 +189,10 @@ let rec pr_module_type pr_c = function
       pr_module_type pr_c mty ++ spc() ++ str" with" ++
       pr_with_declaration pr_c decl
 
+let pr_of_module_type prc (mty,b) =
+  str (if b then ":" else "<:") ++
+  pr_module_type prc mty
+
 let pr_module_vardecls pr_c (l,mty) =
   prlist
     (fun id ->
@@ -203,7 +207,10 @@ let pr_module_binders_list l pr_c = pr_module_binders l pr_c
 
 let rec pr_module_expr = function
   | CMEident qid -> pr_located pr_qualid qid
-  | CMEapply (me1,me2) -> pr_module_expr me1 ++ spc() ++ pr_module_expr me2
+  | CMEapply (me1,(CMEident _ as me2)) ->
+      pr_module_expr me1 ++ spc() ++ pr_module_expr me2
+  | CMEapply (me1,me2) ->
+      pr_module_expr me1 ++ spc() ++ str"(" ++ pr_module_expr me2 ++ str")"
 
 let pr_opt_casted_constr pr_c = function
   | CCast (loc,c,t) -> pr_c c ++ str":" ++ pr_c t
@@ -440,17 +447,18 @@ let rec pr_vernac = function
             str" in" ++ spc() in
       let pr_def_body = function
         | DefineBody (bl,red,c,d) ->
-            let (binds,body) = match c with
-              | CLambdaN (_,bl2,a) when d=None ->
-                  (pr_ne_sep spc (pr_vbinders pr_lconstr) bl ++
-                   spc() ++ pr_binders bl2, a)
-              | _ -> (pr_ne_sep spc (pr_vbinders pr_lconstr) bl, c) in
-            let ty =
-              match d with
-                | None -> mt()
-                | Some t -> spc() ++ str":" ++ pr_lconstrarg t in
+            let (bl2,body,ty) = match d with
+              | None ->
+                  let bl2,body = extract_lam_binders c in
+                  (bl2,body,mt())
+              | Some ty ->
+                  let bl2,body,ty = extract_def_binders c ty in
+                  (bl2,body, spc() ++ str":" ++ pr_lconstrarg ty) in
+            let bindings =
+              pr_ne_sep spc (pr_vbinders pr_lconstr) bl ++
+              if bl2 = [] then mt() else (spc() ++ pr_binders bl2) in
             let ppred = Some (pr_reduce red ++ pr_lconstr body) in
-            (binds,ty,ppred)
+            (bindings,ty,ppred)
         | ProveBody (bl,t) ->
             (pr_vbinders pr_lconstr bl, str" :" ++ pr_lconstrarg t, None) in
       let (binds,typ,c) = pr_def_body b in
@@ -475,8 +483,9 @@ let rec pr_vernac = function
         (pr_assumption_token stre ++ spc() ++ pr_ne_params_list pr_lconstr l)
   | VernacInductive (f,l) ->
       let pr_constructor (coe,(id,c)) =
-        pr_id id ++ spc() ++ (if coe then str":>" else str":")
-        ++ pr_lconstrarg c in
+        hov 2 (pr_id id ++ str" " ++
+               (if coe then str":>" else str":") ++
+               pr_lconstrarg c) in
       let pr_constructor_list l = match l with
         | [] -> mt()
         | _ ->
@@ -490,16 +499,28 @@ let rec pr_vernac = function
         prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_oneind l)
   | VernacFixpoint recs ->
       let pr_onerec = function
-        | (id,_,CProdN(_,bl,type_),CLambdaN(_,_,def)) ->
-            pr_id id ++ spc() ++ pr_binders bl ++ spc()
+        | (id,n,type_0,def0) ->
+            let (bl,def,type_) = extract_def_binders def0 type_0 in
+            let ids = List.flatten (List.map fst bl) in
+            let (bl,def,type_) =
+              if List.length ids <= n then split_fix (n+1) def0 type_0
+              else (bl,def,type_) in
+            let ids = List.flatten (List.map fst bl) in
+            let annot =
+              if List.length ids > 1 then 
+                spc() ++ str "{struct " ++
+                pr_name (snd (List.nth ids n)) ++ str"}"
+              else mt() in
+            pr_id id ++ str" " ++ pr_binders bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr c) type_
-            ++ str" :=" ++ brk(1,1) ++ pr_lconstr def 
-        | _ -> mt() in
+            ++ str" :=" ++ brk(1,1) ++ pr_lconstr def in
       hov 1 (str"Fixpoint" ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)  
   | VernacCoFixpoint corecs ->
       let pr_onecorec (id,c,def) =
-        pr_id id ++ spc() ++ str":" ++ pr_lconstrarg c ++
+        let (bl,def,c) = extract_def_binders def c in
+        pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+        pr_lconstrarg c ++
         str" :=" ++ brk(1,1) ++ pr_lconstr def in
       hov 1 (str"CoFixpoint" ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)  
@@ -549,14 +570,20 @@ let rec pr_vernac = function
   | VernacIdentityCoercion (s,id,c1,c2) -> hov 1 (str"Identity Coercion" ++ (match s with | Decl_kinds.Local -> spc() ++ str"Local" ++ spc() | Decl_kinds.Global -> spc()) ++ pr_id id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
 
   (* Modules and Module Types *)
-  | VernacDeclareModule (id,l,m1,m2) -> hov 1 (str"Module" ++ spc() ++ pr_id id ++ spc() ++ pr_module_binders_list l pr_lconstr ++ (match m1 with
-    | None -> mt()
-    | Some n1 -> str" : " ++ str"TODO" (* pr_module_type pr_constr n1 *) ) ++ (match m2 with
-      | None -> mt()
-      | Some n2 -> str" := " ++ pr_module_expr n2))
-  | VernacDeclareModuleType (id,l,m) -> hov 1 (str"Module Type" ++ spc() ++ pr_id id ++ spc() ++ pr_module_binders_list l pr_lconstr ++ (match m with
-    | None -> mt()
-    | Some n -> str" := " ++ pr_module_type pr_lconstr n))
+  | VernacDefineModule (m,bl,ty,bd) ->
+      hov 2 (str"Module " ++ pr_id m ++ spc() ++
+             pr_module_binders_list bl pr_lconstr ++
+             pr_opt (pr_of_module_type pr_lconstr) ty ++
+             pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd)
+  | VernacDeclareModule (id,l,m1,m2) ->
+      hov 2 (str"Declare Module " ++ pr_id id ++ spc() ++
+             pr_module_binders_list l pr_lconstr ++
+             pr_opt (pr_of_module_type pr_lconstr) m1 ++
+             pr_opt (fun me -> str ":= " ++ pr_module_expr me) m2)
+  | VernacDeclareModuleType (id,l,m) ->
+      hov 2 (str"Module Type " ++ pr_id id ++ spc() ++
+             pr_module_binders_list l pr_lconstr ++
+             pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m)
 
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
@@ -692,13 +719,6 @@ let rec pr_vernac = function
   | VernacV7only _ -> mt()
   | VernacV8only com -> pr_vernac com
   | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te 
-  | VernacDefineModule (m,bl,ty,bd) ->
-      hov 2 (str"Module " ++ pr_id m ++
-      pr_module_binders bl pr_lconstr ++
-      (match ty with
-          None -> mt()
-        | Some(t,_) -> pr_module_type pr_lconstr t) ++
-      pr_opt pr_module_expr bd)
 
 and pr_extend s cl =
   let pr_arg a =