From d5b1c83d0f0a60f9658c45ae902035f2fdef0c41 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 13 Jun 2011 22:21:23 +0000
Subject: Added a flag to restrict conversion in tactic unification on the
 strict subterms of the initial unification problem (inspired from ssreflect
 rewriting strategy). Not activated however (a few applications of setoid
 rewrite use this possibility on closed terms in the stdlib, e.g. "flip le p
 (min n m)" identified with "le (min n m) p").

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14198 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml           | 1 +
 tactics/class_tactics.ml4 | 1 +
 tactics/equality.ml       | 2 ++
 tactics/rewrite.ml4       | 3 +++
 4 files changed, 7 insertions(+)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6780ae2fcf..18e71661ff 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -846,6 +846,7 @@ let auto_unif_flags = {
   resolve_evars = true;
   use_evars_pattern_unification = false;
   frozen_evars = ExistentialSet.empty;
+  restrict_conv_on_strict_subterms = false; (* Compat *)
   modulo_betaiota = false;
   modulo_eta = true;
   allow_K_in_toplevel_higher_order_unification = false
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 3f4e773eca..b460222b95 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -80,6 +80,7 @@ let auto_unif_flags = {
   resolve_evars = false;
   use_evars_pattern_unification = true;
   frozen_evars = ExistentialSet.empty;
+  restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = true;
   modulo_eta = true;
   allow_K_in_toplevel_higher_order_unification = false
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f6e8837f8b..98f47d8fbf 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -88,6 +88,7 @@ let rewrite_unif_flags = {
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
   Unification.frozen_evars = ExistentialSet.empty;
+  Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
   Unification.allow_K_in_toplevel_higher_order_unification = false
@@ -144,6 +145,7 @@ let rewrite_conv_closed_unif_flags = {
   Unification.resolve_evars = false;
   Unification.use_evars_pattern_unification = true;
   Unification.frozen_evars = ExistentialSet.empty;
+  Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
   Unification.allow_K_in_toplevel_higher_order_unification = false
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index b8ebf84a61..821284ec7f 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -308,6 +308,7 @@ let rewrite_unif_flags = {
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
   Unification.frozen_evars = ExistentialSet.empty;
+  Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
   Unification.allow_K_in_toplevel_higher_order_unification = true
@@ -321,6 +322,7 @@ let rewrite2_unif_flags =
      Unification.resolve_evars = true;
      Unification.use_evars_pattern_unification = true;
      Unification.frozen_evars = ExistentialSet.empty;
+     Unification.restrict_conv_on_strict_subterms = false;
      Unification.modulo_betaiota = true;
      Unification.modulo_eta = true;
      Unification.allow_K_in_toplevel_higher_order_unification = true
@@ -335,6 +337,7 @@ let general_rewrite_unif_flags () =
        Unification.resolve_evars = true;
        Unification.use_evars_pattern_unification = true;
        Unification.frozen_evars = ExistentialSet.empty;
+       Unification.restrict_conv_on_strict_subterms = false;
        Unification.modulo_betaiota = true;
        Unification.modulo_eta = true;
        Unification.allow_K_in_toplevel_higher_order_unification = true }
-- 
cgit v1.2.3