Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

7 files changed, 13 insertions, 4 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 041bb44b..f7d63dcd 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1020,6 +1020,7 @@ let auto_unif_flags = {
   use_metas_eagerly_in_conv_on_closed_terms = false;
   modulo_delta = empty_transparent_state;
   modulo_delta_types = full_transparent_state;
+  modulo_delta_in_merge = None;
   check_applied_meta_types = false;
   resolve_evars = true;
   use_pattern_unification = false;
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e8ef545d..cf4a267f 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -77,6 +77,7 @@ let auto_unif_flags = {
   use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = var_full_transparent_state;
   modulo_delta_types = full_transparent_state;
+  modulo_delta_in_merge = None;
   check_applied_meta_types = false;
   resolve_evars = false;
   use_pattern_unification = true;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 241a8bd2..a352355b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -87,6 +87,7 @@ let rewrite_unif_flags = {
   Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
   Unification.modulo_delta = empty_transparent_state;
   Unification.modulo_delta_types = empty_transparent_state;
+  Unification.modulo_delta_in_merge = None;
   Unification.check_applied_meta_types = true;
   Unification.resolve_evars = true;
   Unification.use_pattern_unification = true;
@@ -155,6 +156,7 @@ let rewrite_conv_closed_unif_flags = {
 
   Unification.modulo_delta = empty_transparent_state;
   Unification.modulo_delta_types = full_transparent_state;
+  Unification.modulo_delta_in_merge = None;
   Unification.check_applied_meta_types = true;
   Unification.resolve_evars = false;
   Unification.use_pattern_unification = true;
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index d3403a18..613779c2 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -194,7 +194,7 @@ let pr_in_hyp  pr_id (lo,concl) :  Pp.std_ppcmds =
     | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-"
     | Some l,_ ->
 	str "in" ++
-	  Util.prlist (fun id -> spc () ++ pr_id id) l ++
+         spc () ++ Util.prlist_with_sep Util.pr_comma pr_id l ++
 	  match concl with
 	    | true -> spc () ++ str "|-" ++ spc () ++ str "*"
 	    | _ -> mt ()
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 8a1b5996..47e3b7ca 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -151,8 +151,9 @@ let match_with_disjunction ?(strict=false) t =
   | Ind ind  ->
       let car = mis_constr_nargs ind in
       let (mib,mip) = Global.lookup_inductive ind in
-      if array_for_all (fun ar -> ar = 1) car &&
-	not (mis_is_recursive (ind,mib,mip))
+      if array_for_all (fun ar -> ar = 1) car
+        && not (mis_is_recursive (ind,mib,mip))
+        && (mip.mind_nrealargs = 0)
       then
 	if strict then
 	  if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index dbe61817..b90a911a 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -294,6 +294,7 @@ let rewrite_unif_flags = {
   Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
   Unification.modulo_delta = empty_transparent_state;
   Unification.modulo_delta_types = full_transparent_state;
+  Unification.modulo_delta_in_merge = None;
   Unification.check_applied_meta_types = true;
   Unification.resolve_evars = true;
   Unification.use_pattern_unification = true;
@@ -305,11 +306,12 @@ let rewrite_unif_flags = {
   Unification.allow_K_in_toplevel_higher_order_unification = true
 }
 
-let rewrite2_unif_flags = 
+let rewrite2_unif_flags =
   {  Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
      Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
      Unification.modulo_delta = empty_transparent_state;
      Unification.modulo_delta_types = conv_transparent_state;
+     Unification.modulo_delta_in_merge = None;
      Unification.check_applied_meta_types = true;
      Unification.resolve_evars = true;
      Unification.use_pattern_unification = true;
@@ -327,6 +329,7 @@ let general_rewrite_unif_flags () =
        Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
        Unification.modulo_delta = ts;
        Unification.modulo_delta_types = ts;
+       Unification.modulo_delta_in_merge = None;
        Unification.check_applied_meta_types = true;
        Unification.resolve_evars = true;
        Unification.use_pattern_unification = true;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ff53bfe8..12292196 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1690,6 +1690,7 @@ let default_matching_flags sigma = {
   use_metas_eagerly_in_conv_on_closed_terms = false;
   modulo_delta = empty_transparent_state;
   modulo_delta_types = full_transparent_state;
+  modulo_delta_in_merge = Some full_transparent_state;
   check_applied_meta_types = true;
   resolve_evars = false;
   use_pattern_unification = false;