- Fixed minor bug #1994 in the tactic chapter of the manual [doc]

- Improved warning when found several path to the same file in path
  [mltop.ml4, system.ml]
- Add support for "rewrite" on specific equality to true (i.e. eq_true)
  [Datatypes.v, tactics] 

PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614



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

8 files changed, 29 insertions, 8 deletions

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 28cb402f3..3e3d42263 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1427,7 +1427,7 @@ generally any mutually recursive definitions.
 \begin{Variants}
 \item {\tt Fixpoint {\ident$_1$} {\params$_1$} :{\type$_1$} := {\term$_1$}\\
         with {\ldots} \\
-        with {\ident$_m$} {\params$_m$} :{\type$_m$} :=  {\type$_m$}}\\
+        with {\ident$_m$} {\params$_m$} :{\type$_m$} :=  {\term$_m$}}\\
         Allows to define simultaneously {\ident$_1$}, {\ldots},
         {\ident$_m$}.
 \end{Variants}
diff --git a/lib/system.ml b/lib/system.ml
index 4f21c8746..7ca62dcc8 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -116,7 +116,8 @@ let where_in_path warn path filename =
 	    msg_warning
 	      (str filename ++ str " has been found in" ++ spc () ++
 	       hov 0 (str "[ " ++
-	         hv 0 (prlist_with_sep pr_semicolon (fun (lpe,_) -> str lpe) l)
+	         hv 0 (prlist_with_sep (fun () -> spc() ++ pr_semicolon())
+		   (fun (lpe,_) -> str lpe) l)
 	         ++ str " ];") ++ fnl () ++
 	       str "loading " ++ str f);
 	  (lpe, f) in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index cbcf5993c..641e274af 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -116,13 +116,13 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_
     let sigma = Evd.merge sigma (project gl) in
     let ctype = get_type_of env sigma c' in 
     let rels, t = decompose_prod (whd_betaiotazeta ctype) in
-      match match_with_equation t with
+      match match_with_equality_type t with
       | Some (hdcncl,_) -> (* Fast path: direct leibniz rewrite *)
 	  leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl
       | None ->
 	  let env' = List.fold_left (fun env (n,t) -> push_rel (n, None, t) env) env rels in
 	  let _,t' = splay_prod env' sigma t in (* Search for underlying eq *)
-	    match match_with_equation t' with
+	    match match_with_equality_type t' with
 	    | Some (hdcncl,_) -> (* Maybe a setoid relation with eq inside *)
 		if l = NoBindings && !is_applied_setoid_relation t then
 		  !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 4145a8dcc..9e0281855 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -121,8 +121,8 @@ let match_with_unit_type t =
         let constr_types = mip.mind_nf_lc in 
         let nconstr = Array.length mip.mind_consnames in
         let zero_args c =
-          nb_prod c = mib.mind_nparams in  
-	if nconstr = 1 && array_for_all zero_args constr_types then 
+	  nb_prod c = mib.mind_nparams in  
+	if nconstr = 1 && zero_args constr_types.(0) then 
 	  Some hdapp
         else 
 	  None
@@ -157,6 +157,19 @@ let match_with_equation t =
 
 let is_equation t = op2bool (match_with_equation  t)
 
+let match_with_equality_type t =
+  let (hdapp,args) = decompose_app t in
+  match (kind_of_term hdapp) with
+    | Ind ind when args <> [] -> 
+        let (mib,mip) = Global.lookup_inductive ind in
+        let nconstr = Array.length mip.mind_consnames in
+	if nconstr = 1 && constructor_nrealargs (Global.env()) (ind,1) = 0
+        then 
+	  Some (hdapp,args)
+        else 
+	  None
+    | _ -> None
+
 let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
 
 let match_arrow_pattern t =
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 6dde098cf..ce1c70e5a 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -69,6 +69,9 @@ val is_unit_type           : testing_function
 val match_with_equation    : (constr * constr list) matching_function
 val is_equation            : testing_function 
 
+(* type with only one constructor, no arguments and at least one dependency *)
+val match_with_equality_type : (constr * constr list) matching_function
+
 val match_with_nottype     : (constr * constr) matching_function
 val is_nottype             : testing_function 
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e0f5a3a42..da4d95eaa 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2900,7 +2900,7 @@ let reflexivity_red allowred gl =
   let concl = if not allowred then pf_concl gl
   else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
   in 
-    match match_with_equation concl with
+    match match_with_equality_type concl with
     | None -> None
     | Some _ -> Some (one_constructor 1 NoBindings)
 
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 1e8a5b062..45228073a 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -72,6 +72,10 @@ Hint Resolve andb_true_intro: bool v62.
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
+(** Technical lemma: identify -> rewriting on eq_true with <- rewriting *)
+
+Definition eq_true_ind_r := eq_true_ind.
+
 (** [nat] is the datatype of natural numbers built from [O] and successor [S];
     note that the constructor name is the letter O.
     Numbers in [nat] can be denoted using a decimal notation; 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 275f9a5f7..694e60dbc 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -106,7 +106,7 @@ let dir_ml_load s =
 	 * if this code section starts to use a module not used elsewhere
 	 * in this file, the Makefile dependency logic needs to be updated.
 	 *)
-        let _,gname = where_in_path true !coq_mlpath_copy s in
+        let _,gname = where_in_path true (list_uniquize !coq_mlpath_copy) s in
         try
           Dynlink.loadfile gname;
 	with | Dynlink.Error a ->