*** empty log message ***

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

5 files changed, 13 insertions, 11 deletions

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index c9197ab34c..87f8c8af10 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 4150a09482..5bd871bc9b 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 4fb3fbe38c..b5d6601c66 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 4ae1f280d6..9ff5675884 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 494cf593f2..3941d10c6f 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