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

1 files changed, 3 insertions, 2 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 9b0bb188b..5388bf207 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1138,7 +1138,7 @@ let declare_instance_trans binders a aeq n lemma =
   in anew_instance binders instance 
        [((dummy_loc,id_of_string "transitivity"),[],lemma)]
 
-let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None)) 
+let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor (false,None)))
 
 let declare_relation ?(binders=[]) a aeq n refl symm trans = 
   init_setoid ();
@@ -1421,7 +1421,8 @@ let check_evar_map_of_evars_defs evd =
   Evd.Metaset.iter
    (fun m ->
      if Evd.meta_defined evd m then () else
-      raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
+      raise
+	(Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m])))
  in
   List.iter
    (fun (_,binding) ->