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

2 files changed, 15 insertions, 18 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 10d64dcf8..325debad3 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -55,7 +55,8 @@ let add_ml_include s =
   Mltop.add_ml_dir s
 
 (* Puts dir in the path of ML and in the LoadPath *)
-let coq_add_path s = Mltop.add_path s (Names.make_dirpath [Nameops.coq_root])
+let coq_add_path d s =
+  Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s])
 let coq_add_rec_path s = Mltop.add_rec_path s (Names.make_dirpath [Nameops.coq_root])
 
 (* By the option -include -I or -R of the command line *)
@@ -95,21 +96,21 @@ let theories_dirs_map = [
 
 (* Initializes the LoadPath according to COQLIB and Coq_config *)
 let init_load_path () =
-  (* developper specific directories to open *)
-  let dev = if Coq_config.local then [ "dev" ] else [] in
   let coqlib =
     (* variable COQLIB overrides the default library *)
     getenv_else "COQLIB"
       (if Coq_config.local || !Flags.boot then Coq_config.coqtop
 	else Coq_config.coqlib) in
   let user_contrib = coqlib/"user-contrib" in
-  let dirs = "states" :: "contrib" :: dev in
+  let dirs = "states" :: ["contrib"] in
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
     (* first user-contrib *)
     if Sys.file_exists user_contrib then 
       Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
     (* then states, contrib and dev *)
     List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
+    (* developer specific directory to open *)
+    if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
     (* then standard library *)
     List.iter 
       (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b9f187784..505f456db 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -508,22 +508,19 @@ let explain_typeclass_error env err =
 (* Refiner errors *)
 
 let explain_refiner_bad_type arg ty conclty =
-  str "refiner was given an argument" ++ brk(1,1) ++
+  str "Refiner was given an argument" ++ brk(1,1) ++
   pr_lconstr arg ++ spc () ++
   str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++
   str "instead of" ++ brk(1,1) ++ pr_lconstr conclty
 
-let explain_refiner_occur_meta t =
-  str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr t ++
-  spc () ++ str "because there are metavariables, and it is" ++
-  spc () ++ str "neither an application nor a Case"
-
-let explain_refiner_occur_meta_goal t =
-  str "generated subgoal" ++ brk(1,1) ++ pr_lconstr t ++
-  spc () ++ str "has metavariables in it"
+let explain_refiner_unresolved_bindings l =
+  let l = map_succeed (function Name id -> id | _ -> failwith "") l in
+  str "Unable to find an instance for the " ++ 
+  str (plural (List.length l) "variable") ++ spc () ++
+  prlist_with_sep pr_coma pr_id l
 
 let explain_refiner_cannot_apply t harg =
-  str "in refiner, a term of type " ++ brk(1,1) ++
+  str "In refiner, a term of type " ++ brk(1,1) ++
   pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
   pr_lconstr harg
 
@@ -538,13 +535,12 @@ let explain_does_not_occur_in c hyp =
   str "does not occur in" ++ spc () ++ pr_id hyp ++ str "."
 
 let explain_non_linear_proof c =
-  str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
+  str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
   spc () ++ str "because a metavariable has several occurrences."
 
 let explain_refiner_error = function
   | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
-  | OccurMeta t -> explain_refiner_occur_meta t
-  | OccurMetaGoal t -> explain_refiner_occur_meta_goal t
+  | UnresolvedBindings t -> explain_refiner_unresolved_bindings t
   | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg
   | NotWellTyped c -> explain_refiner_not_well_typed c
   | IntroNeedsProduct -> explain_intro_needs_product ()
@@ -611,7 +607,7 @@ let error_bad_entry () =
   str "Bad inductive definition."
 
 let error_not_allowed_case_analysis dep kind i =
-  str (if dep then "Dependent" else "Non Dependent") ++
+  str (if dep then "Dependent" else "Non dependent") ++
   str " case analysis on sort: " ++ pr_sort kind ++ fnl () ++
   str "is not allowed for inductive definition: " ++
   pr_inductive (Global.env()) i ++ str "."