*** empty log message ***

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

14 files changed, 92 insertions, 45 deletions

diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 49a187caa..c67dea9aa 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -107,6 +107,19 @@ let _ = Tacinterp.add_genarg_interp "minus_div_arg"
 	  (in_gen (wit_pair (wit_opt rawwit_constr) (wit_opt rawwit_constr))
 	    (out_gen rawwit_minus_div_arg x))))))
 
+open Ppconstrnew
+let pp_minus_div_arg (omin,odiv) = str "still no printer for minus_div_arg"
+let pp_raw_minus_div_arg (omin,odiv) =
+  if omin=None && odiv=None then mt() else
+    spc() ++ str "with" ++
+    pr_opt (fun c -> str "minus := " ++ pr_constr c) omin ++
+    pr_opt (fun c -> str "div := " ++ pr_constr c) odiv
+
+let () =
+  Pptactic.declare_extra_genarg_pprule true
+    (rawwit_minus_div_arg,pp_raw_minus_div_arg)
+    (wit_minus_div_arg,pp_minus_div_arg)
+
 open Pcoq.Constr
 GEXTEND Gram
   GLOBAL: minus_div_arg;
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index c9197ab34..87f8c8af1 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -259,7 +259,7 @@ let filter_by_module_from_varg_list l =
 let add_search (global_reference:global_reference) assumptions cstr =
   try 
   let id_string =
-    string_of_qualid (Nametab.shortest_qualid_of_global None 
+    string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty
 			global_reference) in
   let ast = 
     try
@@ -323,10 +323,10 @@ let globcv x =
     match x with
       | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
 	    convert_qualid
-	      (Nametab.shortest_qualid_of_global None (IndRef(sp,tyi)))
+	      (Nametab.shortest_qualid_of_global Idset.empty (IndRef(sp,tyi)))
       | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
 	  convert_qualid
-            (Nametab.shortest_qualid_of_global None
+            (Nametab.shortest_qualid_of_global Idset.empty
 	       (ConstructRef ((sp, tyi), i)))
   | _ -> failwith "globcv : unexpected value";;
 
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 4150a0948..5bd871bc9 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -114,7 +114,7 @@ let convert_one_inductive sp tyi =
   let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
   let env = Global.env () in
   let envpar = push_rel_context params env in
-  let sp = sp_of_global None (IndRef (sp, tyi)) in
+  let sp = sp_of_global (IndRef (sp, tyi)) in
   (basename sp,
    convert_env(List.rev params),
    (extern_constr true envpar arity),
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 4fb3fbe38..b5d6601c6 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -158,7 +158,7 @@ let make_pbp_atomic_tactic = function
   | PbpTryAssumption (Some a) ->
       TacTry (TacAtom (zz, TacExact (make_var a)))
   | PbpExists x -> 
-      TacAtom (zz, TacSplit (ImplicitBindings [make_pbp_pattern x]))
+      TacAtom (zz, TacSplit (true,ImplicitBindings [make_pbp_pattern x]))
   | PbpGeneralize (h,args) ->
       let l = List.map make_pbp_pattern args in
       TacAtom (zz, TacGeneralize [make_app (make_var h) l])
@@ -176,7 +176,7 @@ let make_pbp_atomic_tactic = function
 	(zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
       TacTry (TacAtom (zz, TacClear (List.map (fun s -> AN s) l)))
-  | PbpSplit -> TacAtom (zz, TacSplit NoBindings);;
+  | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));;
 
 let rec make_pbp_tactic = function
   | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 4ae1f280d..9ff567588 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1271,8 +1271,8 @@ let rec natural_ntree ig ntree =
 	    TacIntroPattern _ -> natural_intros ig lh g gs ltree
 	  | TacIntroMove _ -> natural_intros ig lh g gs ltree
 	  | TacFix (_,n) -> natural_fix ig lh g gs n ltree
-	  | TacSplit NoBindings -> natural_split ig lh g gs ge [] ltree
-	  | TacSplit(ImplicitBindings l) -> natural_split ig lh g gs ge l ltree
+	  | TacSplit (_,NoBindings) -> natural_split ig lh g gs ge [] ltree
+	  | TacSplit(_,ImplicitBindings l) -> natural_split ig lh g gs ge l ltree
 	  | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree
 	  | TacRight _ -> natural_right ig lh g gs ltree
 	  | TacLeft _ -> natural_left ig lh g gs ltree
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 494cf593f..3941d10c6 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -822,7 +822,8 @@ and xlate_tac =
     | TacIntroMove (None, None) ->  CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
     | TacLeft bindl -> CT_left (xlate_bindings bindl)
     | TacRight bindl -> CT_right (xlate_bindings bindl)
-    | TacSplit bindl -> CT_split (xlate_bindings bindl)
+    | TacSplit (false,bindl) -> CT_split (xlate_bindings bindl)
+    | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl)
     | TacExtend (_,"Replace", [c1; c2]) ->
      let c1 = xlate_formula (out_gen rawwit_constr c1) in
      let c2 = xlate_formula (out_gen rawwit_constr c2) in
@@ -1581,13 +1582,14 @@ let xlate_vernac =
         CT_coerce_NONE_to_STRING_OPT CT_none)
    | VernacRequire (_,_,([]|_::_::_)) ->
        xlate_error "TODO: general form of future Require"
-   | VernacRequireFrom (impexp, spec, filename) ->
+   | VernacRequireFrom (Some impexp, spec, filename) ->
       let ct_impexp, ct_spec = get_require_flags impexp spec 
       and id = id_of_string (Filename.basename filename)
       in
       CT_require
        (ct_impexp, ct_spec, xlate_ident id, 
          CT_coerce_STRING_to_STRING_OPT (CT_string filename))
+   | VernacRequireFrom (None, _, _) -> xlate_error "TODO: Read Module"
 
    | VernacSyntax (phylum, l) -> xlate_error "SYNTAX not implemented"
        (*Two versions of the syntax node with and without the binder list. *)
@@ -1607,7 +1609,7 @@ let xlate_vernac =
 
    | VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented"
 
-   | VernacInfix (str_assoc, n, str, id, false, None) ->
+   | VernacInfix (str_assoc, n, str, id, false, _, None) ->
       CT_infix (
        (match str_assoc with
         | Some Gramext.LeftA -> CT_lefta
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 4373da462..651b808c0 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -151,7 +151,7 @@ let dest_const_apply t =
     | Ind isp       -> IndRef isp
     | _ -> raise Destruct
   in
-  id_of_global None ref, args
+  id_of_global ref, args
 
 type result = 
   | Kvar of string
@@ -164,11 +164,11 @@ let destructurate t =
 (*  let env = Global.env() in*)
   match kind_of_term c, args with
     | Const sp, args ->
-	Kapp (string_of_id (id_of_global None (ConstRef sp)),args)
+	Kapp (string_of_id (id_of_global (ConstRef sp)),args)
     | Construct csp , args ->
-	Kapp (string_of_id (id_of_global None (ConstructRef csp)), args)
+	Kapp (string_of_id (id_of_global (ConstructRef csp)), args)
     | Ind isp, args ->
-	Kapp (string_of_id (id_of_global None (IndRef isp)),args)
+	Kapp (string_of_id (id_of_global (IndRef isp)),args)
     | Var id,[] -> Kvar(string_of_id id)
     | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
     | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 1c48c4b45..08bb53955 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -25,8 +25,8 @@ Variable Azero : A.
   is a good choice. The proof of A_eq_prop is in this case easy. *)
 Variable Aeq : A -> A -> bool.
 
-Infix 4 "+" Aplus.
-Infix 4 "*" Amult.
+Infix 4 "+" Aplus V8only 40 (left associativity).
+Infix 4 "*" Amult V8only 30 (left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
 
@@ -146,11 +146,16 @@ Variable Azero : A.
 Variable Aopp : A -> A.
 Variable Aeq : A -> A -> bool.
 
-Infix 4 "+" Aplus.
-Infix 4 "*" Amult.
+Infix 4 "+" Aplus V8only 40 (left associativity).
+Infix 4 "*" Amult V8only 30 (left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
-Notation "- x" := (Aopp x) (at level 3).
+Notation "- 0" := (Aopp Azero) (at level 3)
+  V8only (at level 40, left associativity).
+Notation "- 1" := (Aopp Aone) (at level 3)
+  V8only (at level 40, left associativity).
+Notation "- x" := (Aopp x) (at level 3)
+  V8only (at level 40, left associativity).
 
 Record Ring_Theory : Prop :=
 { Th_plus_sym  : (n,m:A) n + m == m + n;
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index 3456b1051..4fc7ea104 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -18,7 +18,8 @@ Section Setoid_rings.
 Variable A : Type.
 Variable Aequiv : A -> A -> Prop.
 
-Infix "==" Aequiv (at level 5).
+Infix "==" Aequiv (at level 5)
+  V8only (at level 50).
 
 Variable S : (Setoid_Theory A Aequiv).
 
@@ -31,11 +32,16 @@ Variable Azero : A.
 Variable Aopp : A -> A.
 Variable Aeq : A -> A -> bool.
 
-Infix "+" Aplus (at level 4).
-Infix "*" Amult (at level 3).
+Infix 4 "+" Aplus V8only 40 (left associativity).
+Infix 4 "*" Amult V8only 30 (left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
-Notation "- x" := (Aopp x) (at level 3).
+Notation "- 0" := (Aopp Azero) (at level 3)
+  V8only (at level 40, left associativity).
+Notation "- 1" := (Aopp Aone) (at level 3)
+  V8only (at level 40, left associativity).
+Notation "- x" := (Aopp x) (at level 3)
+  V8only (at level 40, left associativity).
 
 Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2.
 Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2.
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 95e4a5f5a..ef35d3245 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -642,25 +642,46 @@ Recursive Tactic Definition loop t := (
   | [(Topp ?1)] -> (loop ?1)
   | [(Tint ?1)] -> (loop ?1)
   (* Eliminations *)
-  | [(Case ?1 of ? ? ? ?   ? ? ? ?  ? end)] -> 
+  | [(Cases ?1 of
+        | (EqTerm _ _) => ?
+        | (LeqTerm _ _) => ?
+        | TrueTerm => ?
+        | FalseTerm => ?
+        | (Tnot _) => ?
+        | (GeqTerm _ _) => ?
+        | (GtTerm _ _) => ?
+        | (LtTerm _ _) => ?
+        | (NeqTerm _ _) => ?
+        end)] -> 
        (Case ?1; [ Intro; Intro | Intro; Intro | Idtac | Idtac 
                  | Intro | Intro; Intro | Intro; Intro | Intro; Intro
                  | Intro; Intro ]);
         Auto; Simplify
-  | [(Case ?1 of ? ? ? ? ? ? end)] -> 
+  | [(Cases ?1 of
+        (Tint _) => ?
+      | (Tplus _ _) => ?
+      | (Tmult _ _) => ?
+      | (Tminus _ _) => ?
+      | (Topp _) => ?
+      | (Tvar _) => ?
+      end)] -> 
        (Case ?1; [ Intro | Intro; Intro | Intro; Intro | Intro; Intro | 
                    Intro | Intro ]); Auto; Simplify
-  | [(Case (Zcompare ?1 ?2) of ? ? ? end)] -> 
+  | [(Cases (Zcompare ?1 ?2) of
+        EGAL => ?
+      | INFERIEUR => ?
+      | SUPERIEUR => ?
+      end)] -> 
        (Elim_Zcompare ?1 ?2) ; Intro ; Auto; Simplify
-  | [(Case ?1 of ? ? ? end)] -> 
+  | [(Cases ?1 of ZERO => ? | (POS _) => ? | (NEG _) => ? end)] -> 
        (Case ?1; [ Idtac | Intro | Intro ]); Auto; Simplify
-  | [(Case (eq_Z ?1 ?2) of ? ? end)] -> 
+  | [(if (eq_Z ?1 ?2) then ? else ?)] -> 
        ((Elim_eq_Z ?1 ?2); Intro H; [Rewrite H; Clear H | Clear H]);
        Simpl; Auto; Simplify
-  | [(Case (eq_term ?1 ?2) of ? ? end)] -> 
+  | [(if (eq_term ?1 ?2) then ? else ?)] -> 
        ((Elim_eq_term ?1 ?2); Intro H; [Rewrite H; Clear H | Clear H]); 
        Simpl; Auto; Simplify
-  | [(Case (eq_pos ?1 ?2) of ? ? end)] -> 
+  | [(if (eq_pos ?1 ?2) then ? else ?)] -> 
        ((Elim_eq_pos ?1 ?2); Intro H; [Rewrite H; Clear H | Clear H]);
        Simpl; Auto; Simplify
   | _ -> Fail)
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 42b61a150..8b055e296 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -21,15 +21,15 @@ let destructurate t =
   match Term.kind_of_term c, args with
     | Term.Const sp, args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global None (Libnames.ConstRef sp)),
+		(Nametab.id_of_global (Libnames.ConstRef sp)),
               args)
     | Term.Construct csp , args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global None (Libnames.ConstructRef csp)),
+		(Nametab.id_of_global (Libnames.ConstructRef csp)),
 	        args)
     | Term.Ind isp, args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global None (Libnames.IndRef isp)),args)
+		(Nametab.id_of_global (Libnames.IndRef isp)),args)
     | Term.Var id,[] -> Kvar(Names.string_of_id id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
@@ -47,7 +47,7 @@ let dest_const_apply t =
     | Term.Ind isp       -> Libnames.IndRef isp
     | _ -> raise Destruct
   in
-  Nametab.id_of_global None ref, args
+  Nametab.id_of_global ref, args
 
 let recognize_number t =
   let rec loop t =
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index c0bdf07a3..b3d164122 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -254,11 +254,11 @@ print_endline "PASSATO" ; flush stdout ;
                 match g with
                    Libnames.ConstructRef ((induri,_),_)
                  | Libnames.IndRef (induri,_) ->
-                    Nametab.sp_of_global None (Libnames.IndRef (induri,0))
+                    Nametab.sp_of_global (Libnames.IndRef (induri,0))
                  | Libnames.VarRef id ->
                     (* Invariant: variables are never cooked in Coq *)
                     raise Not_found
-                 | _ -> Nametab.sp_of_global None g
+                 | _ -> Nametab.sp_of_global g
                in
                Dischargedhypsmap.get_discharged_hyps sp,
                get_module_path_of_section_path sp
diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index e2b49a391..1ee1ef4ea 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -420,18 +420,18 @@ let print_term inner_types l env csr =
        >]
 )
    | T.Const kn ->
-       let sp = Nt.sp_of_global None (L.ConstRef kn) in  
+       let sp = Nt.sp_of_global (L.ConstRef kn) in  
 	 X.xml_empty "CONST"
        (add_sort_attribute false
         ["uri",(uri_of_path sp Constant) ; "id", next_id])
    | T.Ind (kn,i) ->
-      let sp = Nt.sp_of_global None (L.IndRef(kn,0)) in  
+      let sp = Nt.sp_of_global (L.IndRef(kn,0)) in  
       X.xml_empty "MUTIND"
        ["uri",(uri_of_path sp Inductive) ;
         "noType",(string_of_int i) ;
         "id", next_id]
    | T.Construct ((kn,i),j) ->
-      let sp = Nt.sp_of_global None (L.IndRef(kn,0)) in  
+      let sp = Nt.sp_of_global (L.IndRef(kn,0)) in  
       X.xml_empty "MUTCONSTRUCT"
        (add_sort_attribute false
         ["uri",(uri_of_path sp Inductive) ;
@@ -439,7 +439,7 @@ let print_term inner_types l env csr =
          "noConstr",(string_of_int j) ;
          "id", next_id])
    | T.Case ({T.ci_ind=(kn,i)},ty,term,a) ->
-      let sp = Nt.sp_of_global None (L.IndRef(kn,0)) in  
+      let sp = Nt.sp_of_global (L.IndRef(kn,0)) in  
       let (uri, typeno) = (uri_of_path sp Inductive),i in
        X.xml_nempty "MUTCASE"
         (add_sort_attribute true
@@ -728,7 +728,7 @@ let print (_,qid as locqid) fn =
        let (_,body,typ) = G.lookup_named id in
         sp,Variable,print_variable id body (T.body_of_type typ) env inner_types
     | Ln.ConstRef kn ->
-       let sp = Nt.sp_of_global None glob_ref in
+       let sp = Nt.sp_of_global glob_ref in
        let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
         G.lookup_constant kn in
        let hyps = string_list_of_named_context_list hyps in
@@ -742,7 +742,7 @@ let print (_,qid as locqid) fn =
 	      print_definition id c typ [] hyps env inner_types
         end
     | Ln.IndRef (kn,_) ->
-       let sp = Nt.sp_of_global None (Ln.IndRef(kn,0)) in  
+       let sp = Nt.sp_of_global (Ln.IndRef(kn,0)) in  
        let {D.mind_packets=packs ;
             D.mind_hyps=hyps;
             D.mind_finite=finite} = G.lookup_mind kn in
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
index bcfcbd2ff..2807a3d6e 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/contrib/xml/xmlentries.ml4
@@ -50,7 +50,7 @@ END
 let pr_filename = function Some fn -> str " File" ++ str fn | None -> mt ()
 
 let _ = 
-  Pptactic.declare_extra_genarg_pprule 
+  Pptactic.declare_extra_genarg_pprule true
     (rawwit_filename, pr_filename)
     (wit_filename, pr_filename)
 
@@ -76,7 +76,7 @@ open Pp
 let pr_diskname = function Some fn -> str " Disk" ++ str fn | None -> mt ()
 
 let _ = 
-  Pptactic.declare_extra_genarg_pprule 
+  Pptactic.declare_extra_genarg_pprule true
     (rawwit_diskname, pr_diskname)
     (wit_diskname, pr_diskname)