From 218545f49ea41ff12fd8c8f2c094e333be9d0f7e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 17 Dec 2011 22:59:36 +0000
Subject: Added a flag to control the use of typing when instantiating applied
 meta in the tactic unification algorithm ("auto" becomes much slower if it
 takes into account the type of metas).

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

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e15c30a3b5..93ca89f47a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1021,6 +1021,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;
+  check_applied_meta_types = false;
   resolve_evars = true;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true;
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e219bbff09..42df244def 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;
+  check_applied_meta_types = false;
   resolve_evars = false;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 76bceb738f..10fd0fef9e 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.check_applied_meta_types = true;
   Unification.resolve_evars = true;
   Unification.use_pattern_unification = true;
   Unification.use_meta_bound_pattern_unification = true;
@@ -154,6 +155,7 @@ let rewrite_conv_closed_unif_flags = {
 
   Unification.modulo_delta = empty_transparent_state;
   Unification.modulo_delta_types = full_transparent_state;
+  Unification.check_applied_meta_types = true;
   Unification.resolve_evars = false;
   Unification.use_pattern_unification = true;
     (* To rewrite "?n x y" in "y+x=0" when ?n is *)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 80930af42c..d297969d1f 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -299,6 +299,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.check_applied_meta_types = true;
   Unification.resolve_evars = true;
   Unification.use_pattern_unification = true;
   Unification.use_meta_bound_pattern_unification = true;
@@ -314,6 +315,7 @@ let rewrite2_unif_flags =
      Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
      Unification.modulo_delta = empty_transparent_state;
      Unification.modulo_delta_types = conv_transparent_state;
+     Unification.check_applied_meta_types = true;
      Unification.resolve_evars = true;
      Unification.use_pattern_unification = true;
      Unification.use_meta_bound_pattern_unification = true;
@@ -330,6 +332,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.check_applied_meta_types = true;
        Unification.resolve_evars = true;
        Unification.use_pattern_unification = true;
        Unification.use_meta_bound_pattern_unification = true;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1b35888c03..988d9f5308 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;
+  check_applied_meta_types = true;
   resolve_evars = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = false;
-- 
cgit v1.2.3