Bugs, nettoyage, et améliorations diverses

- vérification de la cohérence des ident pour éviter une option -R
  avec des noms non parsables (la vérification est faite dans
  id_of_string ce qui est très exigeant; faudrait-il une solution plus
  souple ?)
- correction message d'erreur inapproprié dans le apply qui descend dans les 
  conjonctions
- nettoyage autour de l'échec en présence de métas dans le prim_refiner
- nouveau message d'erreur quand des variables ne peuvent être instanciées
- quelques simplifications et davantage de robustesse dans inversion
- factorisation du code de constructor and co avec celui de econstructor and co

Documentation des tactiques
- edestruct/einduction/ecase/eelim et nouveautés apply
- nouvelle sémantique des intropatterns disjonctifs et documentation des
  pattern -> et <-
- relecture de certaines parties du chapitre tactique


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

12 files changed, 34 insertions, 42 deletions

diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index fe41b96cbb..ac32f6abee 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -120,7 +120,7 @@ type side = Hyp | Concl | Hint
 
 let no_atoms = (false,{positive=[];negative=[]})
 
-let dummy_id=VarRef (id_of_string "")
+let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *)
 
 let build_atoms gl metagen side cciterm =
   let trivial =ref false
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index a181851680..b6112e653d 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -78,7 +78,7 @@ let and_tac backtrack continue seq=
 
 let or_tac backtrack continue seq=
   tclORELSE 
-    (any_constructor (Some (tclCOMPLETE (wrap 0 true continue seq))))
+    (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq))))
     backtrack
 
 let arrow_tac backtrack continue seq=
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index c5f8509759..d1527c58ad 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -337,11 +337,11 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacRevert    _ -> acc
 
     (* Constructors *)
-    | TacLeft        cb
-    | TacRight       cb
-    | TacSplit       (_, cb)
-    | TacConstructor (_, cb) -> depends_of_'a_bindings depends_of_'constr cb acc
-    | TacAnyConstructor taco -> Option.fold_right depends_of_'tac taco acc
+    | TacLeft        (_,cb)
+    | TacRight       (_,cb)
+    | TacSplit       (_, _, cb)
+    | TacConstructor (_, _, cb) -> depends_of_'a_bindings depends_of_'constr cb acc
+    | TacAnyConstructor (_,taco) -> Option.fold_right depends_of_'tac taco acc
 
     (* Conversion *)
     | TacReduce  (reg,_) ->
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 0680cc23e5..c16cde7d72 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -163,12 +163,12 @@ let make_pbp_atomic_tactic = function
   | PbpTryAssumption (Some a) ->
       TacTry (TacAtom (zz, TacExact (make_var a)))
   | PbpExists x -> 
-      TacAtom (zz, TacSplit (true,ImplicitBindings [make_pbp_pattern x]))
+      TacAtom (zz, TacSplit (false,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])
-  | PbpLeft -> TacAtom (zz, TacLeft NoBindings)
-  | PbpRight -> TacAtom (zz, TacRight NoBindings)
+  | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings))
+  | PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
   | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
   | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings)))
@@ -178,7 +178,7 @@ let make_pbp_atomic_tactic = function
 	(zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
       TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l)))
-  | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));;
+  | PbpSplit -> TacAtom (zz, TacSplit (false,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 20c1cc04f5..7f20196818 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1183,8 +1183,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 (List.map snd l) ltree
+	  | TacSplit (_,_,NoBindings) -> natural_split ig lh g gs ge [] ltree
+	  | TacSplit(_,_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree
 	  | TacGeneralize l -> natural_generalize ig lh g gs ge (List.map snd 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 63efd543aa..16a95d065c 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -976,10 +976,12 @@ and xlate_tac =
     | TacIntroMove (Some id, None) ->
      CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)])
     | 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 (false,bindl) -> CT_split (xlate_bindings bindl)
-    | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl)
+    | TacLeft (false,bindl) -> CT_left (xlate_bindings bindl)
+    | TacRight (false,bindl) -> CT_right (xlate_bindings bindl)
+    | TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl)
+    | TacSplit (false,true,bindl) -> CT_exists (xlate_bindings bindl)
+    | TacSplit _ | TacRight _ | TacLeft _ -> 
+	xlate_error "TODO: esplit, eright, etc"
     | TacExtend (_,"replace", [c1; c2;cl;tac_opt]) ->
 	let c1 = xlate_formula (out_gen rawwit_constr c1) in
 	let c2 = xlate_formula (out_gen rawwit_constr c2) in
@@ -1149,9 +1151,10 @@ and xlate_tac =
     | TacApply (true,true,(c,bindl)) ->
      CT_eapply (xlate_formula c, xlate_bindings bindl)
     | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply"
-    | TacConstructor (n_or_meta, bindl) ->
+    | TacConstructor (false,n_or_meta, bindl) ->
 	let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
 	in CT_constructor (CT_int n, xlate_bindings bindl)
+    | TacConstructor _ -> xlate_error "TODO: econstructor"
     | TacSpecialize (nopt, (c,sl)) ->
      CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl)
     | TacGeneralize [] -> xlate_error ""
@@ -1239,11 +1242,12 @@ and xlate_tac =
         CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
     | TacAssert _ ->
 	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
-    | TacAnyConstructor(Some tac) -> 
+    | TacAnyConstructor(false,Some tac) -> 
 	CT_any_constructor
 	(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
-    | TacAnyConstructor(None) -> 
+    | TacAnyConstructor(false,None) -> 
 	CT_any_constructor(CT_coerce_NONE_to_TACTIC_OPT CT_none)
+    | TacAnyConstructor _ -> xlate_error "TODO: econstructor"
     | TacExtend(_, "ring", [args]) -> 
 	CT_ring
 	  (CT_formula_list
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index aa59daf5fa..b96b57d5bc 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -128,7 +128,7 @@ let intern_id,unintern_id =
     
 let mk_then = tclTHENLIST
 
-let exists_tac c = constructor_tac (Some 1) 1 (Rawterm.ImplicitBindings [c])
+let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c])
 
 let generalize_tac t = generalize_time (generalize t)
 let elim t = elim_time (simplest_elim t)
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 1bc5897c45..6863a18855 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1705,7 +1705,7 @@ let vars_of_ctx ctx =
 	    match na with
 		Anonymous -> raise (Invalid_argument "vars_of_ctx")
 	      | Name n -> n, RVar (dummy_loc, n) :: vars)
-      ctx (id_of_string "vars_of_ctx: error", [])
+      ctx (id_of_string "vars_of_ctx_error", [])
   in List.rev y
 
 let rec is_included x y = 
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index cb3873bdfb..2a8e2e5d90 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -79,7 +79,7 @@ let type_ctx_instance isevars env ctx inst subst =
 	(na, c) :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
 
-let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))
+(*let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))*)
 
 let type_class_instance_params isevars env id n ctx inst subst =
   List.fold_left2
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index dc79597dd4..91bf626b10 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -238,7 +238,7 @@ let build_dependent_sum l =
 	     (tclTHENS tac
 		([intros;
 		  (tclTHENSEQ 
-		     [constructor_tac (Some 1) 1 
+		     [constructor_tac false (Some 1) 1 
 			(Rawterm.ImplicitBindings [inj_open (mkVar n)]);
 		      cont]);
 		 ])))
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 75e428e14d..5515320f0a 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -57,16 +57,6 @@ let remove_module_dirpath_from_dirpath ~basedir dir =
 let get_uri_of_var v pvars =
  let module D = Declare in
  let module N = Names in
-  let rec search_in_pvars names =
-   function
-      [] -> None
-    | ((name,l)::tl) ->
-       let names' = name::names in
-        if List.mem v l then
-         Some names'
-        else
-         search_in_pvars names' tl
-  in
   let rec search_in_open_sections =
    function
       [] -> Util.error ("Variable "^v^" not found")
@@ -78,9 +68,10 @@ let get_uri_of_var v pvars =
          search_in_open_sections tl
   in
    let path =
-    match search_in_pvars [] pvars with
-       None -> search_in_open_sections (N.repr_dirpath (Lib.cwd ()))
-     | Some path -> path
+    if List.mem v pvars then
+      []
+    else
+      search_in_open_sections (N.repr_dirpath (Lib.cwd ()))
    in
     "cic:" ^
      List.fold_left
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 3a0fdfb9b9..649139f356 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -89,8 +89,7 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
 (* OF VARIABLES DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT   *)
 (* SECTION, WHOSE PATH IS namei                                     *)
 
-let pvars =
- ref ([Names.id_of_string "",[]] : (Names.identifier * string list) list);;
+let pvars = ref ([] : string list);;
 let cumenv = ref Environ.empty_env;;
 
 (* filter_params pvars hyps *)
@@ -138,9 +137,7 @@ let add_to_pvars x =
          E.push_named (Names.id_of_string v, None, typ) !cumenv ;
        v
   in
-   match !pvars with
-      []       -> assert false
-    | ((name,l)::tl) -> pvars := (name,v::l)::tl
+  pvars := v::!pvars
 ;;
 
 (* The computation is very inefficient, but we can't do anything *)