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
---
 proofs/clenv.ml    | 7 ++++++-
 proofs/clenvtac.ml | 1 +
 2 files changed, 7 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 35552b8d85..8c05499a2f 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -356,7 +356,12 @@ let connect_clenv gls clenv =
 
    In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
 *)
-let clenv_fchain ?(flags=elim_flags) mv clenv nextclenv =
+
+let fchain_flags =
+  { default_unify_flags with
+    allow_K_in_toplevel_higher_order_unification = true }
+
+let clenv_fchain ?(flags=fchain_flags) mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
   let clenv' =
     { templval = clenv.templval;
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index dad4b5041e..a266405f7a 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -108,6 +108,7 @@ let fail_quick_unif_flags = {
   resolve_evars = false;
   use_evars_pattern_unification = false;
   frozen_evars = ExistentialSet.empty;
+  restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
   modulo_eta = true;
   allow_K_in_toplevel_higher_order_unification = false
-- 
cgit v1.2.3