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, 9 insertions, 7 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 242368ce99..e5632515d0 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -261,8 +261,8 @@ let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
  * pose a value for it by constructing a fresh evar.  We do this in
  * left-to-right order, so that every evar's type is always closed w.r.t.
  * metas. *)
-let clenv_pose_dependent_evars clenv =
-  let dep_mvs = clenv_dependent false clenv in
+
+let clenv_pose_metas_as_evars clenv dep_mvs =
   List.fold_left
     (fun clenv mv ->
       let ty = clenv_meta_type clenv mv in
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 4f27ec902f..dfa7513495 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -79,7 +79,9 @@ val clenv_unique_resolver :
 val evar_clenv_unique_resolver :
   bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv
 
-val clenv_pose_dependent_evars : clausenv -> clausenv
+val clenv_dependent : bool -> clausenv -> metavariable list
+
+val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
 
 (***************************************************************)
 (* Bindings *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 2703e5ae0c..91b70e3b02 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -674,5 +674,5 @@ let pr_evar_defs evd =
       str"METAS:"++brk(0,1)++pr_meta_map evd.metas in
   v 0 (pp_evm ++ cstrs ++ pp_met)
 
-let pr_metaset metas =
-  Metaset.fold (fun mv pp -> pr_meta mv ++ pp) metas (Pp.mt())
+let pr_metaset metas = 
+  str "[" ++ prlist_with_sep spc pr_meta (Metaset.elements metas) ++ str "]"
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 90a3728ebb..05af1652e1 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -92,7 +92,7 @@ let head_of_constr_reference c = match kind_of_term c with
 let rec pattern_of_constr t =
   match kind_of_term t with
     | Rel n  -> PRel n
-    | Meta n -> PMeta (Some (id_of_string (string_of_int n)))
+    | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
     | Sort (Prop c) -> PSort (RProp c)
     | Sort (Type _) -> PSort (RType None)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 32df490db8..ece3586a19 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -23,7 +23,7 @@ open Evd
 let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
-    with Not_found -> error ("unknown meta ?"^string_of_int mv) in
+    with Not_found -> anomaly ("unknown meta ?"^Nameops.string_of_meta mv) in
   meta_instance evd ty
 
 let constant_type_knowing_parameters env cst jl =