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

5 files changed, 27 insertions, 14 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index d133beaa9..60abc5d66 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -60,8 +60,16 @@ let clenv_cast_meta clenv =
   in 
   crec
 
+let clenv_pose_dependent_evars with_evars clenv =
+  let dep_mvs = clenv_dependent false clenv in
+  if dep_mvs <> [] & not with_evars then
+    raise
+      (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
+  clenv_pose_metas_as_evars clenv dep_mvs
+
+
 let clenv_refine with_evars clenv gls =
-  let clenv = if with_evars then clenv_pose_dependent_evars clenv else clenv in
+  let clenv = clenv_pose_dependent_evars with_evars clenv in
   tclTHEN
     (tclEVARS (evars_of clenv.evd)) 
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 90d010c80..0cf0a5545 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -26,5 +26,7 @@ val clenv_refine : evars_flag -> clausenv -> tactic
 val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
 
+val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
+
 (* Compatibility, use res_pf ?with_evars:true instead *)
 val e_res_pf : clausenv -> tactic
diff --git a/proofs/logic.ml b/proofs/logic.ml
index c9ae78103..24de605ac 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -32,8 +32,7 @@ type refiner_error =
 
   (* Errors raised by the refiner *)
   | BadType of constr * constr * constr
-  | OccurMeta of constr
-  | OccurMetaGoal of constr
+  | UnresolvedBindings of name list
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
@@ -266,8 +265,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 *)
   match kind_of_term trm with
     | Meta _ ->
-	if occur_meta conclty then
-          raise (RefinerError (OccurMetaGoal conclty));
+	if !check && occur_meta conclty then
+	  anomaly "refined called with a dependent meta";
 	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
 
     | Cast (t,_, ty) ->
@@ -302,7 +301,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	(acc'',conclty')
 
     | _ -> 
-	if occur_meta trm then raise (RefinerError (OccurMeta trm));
+	if occur_meta trm then
+	  anomaly "refiner called with a meta in non app/case subterm";
       	let t'ty = goal_type_of env sigma trm in
 	check_conv_leq_goal env sigma trm t'ty conclty;
         (goalacc,t'ty)
@@ -342,7 +342,10 @@ and mk_hdgoals sigma goal goalacc trm =
 	in
 	(acc'',conclty')
 
-    | _ -> goalacc, goal_type_of env sigma trm
+    | _ ->
+	if !check && occur_meta trm then
+	  anomaly "refined called with a dependent meta";
+	goalacc, goal_type_of env sigma trm
 
 and mk_arggoals sigma goal goalacc funty = function
   | [] -> goalacc,funty
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 081d02f37..88e77fd7b 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -50,8 +50,7 @@ type refiner_error =
 
   (*i Errors raised by the refiner i*)
   | BadType of constr * constr * constr
-  | OccurMeta of constr
-  | OccurMetaGoal of constr
+  | UnresolvedBindings of name list
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 595c2ec9b..7a90040e5 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -24,6 +24,7 @@ type lazy_flag = bool      (* true = lazy             false = eager *)
 type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
+type split_flag = bool     (* true = exists           false = split *)
 
 type raw_red_flag =
   | FBeta
@@ -179,11 +180,11 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacRevert of 'id list
 
   (* Constructors *)
-  | TacLeft of 'constr bindings
-  | TacRight of 'constr bindings
-  | TacSplit of bool * 'constr bindings
-  | TacAnyConstructor of 'tac option
-  | TacConstructor of int or_metaid * 'constr bindings
+  | TacLeft of evars_flag * 'constr bindings
+  | TacRight of evars_flag * 'constr bindings
+  | TacSplit of evars_flag * split_flag * 'constr bindings
+  | TacAnyConstructor of evars_flag * 'tac option
+  | TacConstructor of evars_flag * int or_metaid * 'constr bindings
 
   (* Conversion *)
   | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause