From 880a83169c1d1df8726d301a9f8a9fc845cc7d1e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 21 Apr 2008 13:57:03 +0000
Subject: - Parameterize unification by two sets of transparent_state, one for
 open term unification (for constant and variable delta unfolding) and one to
 parameterize closed-term conversion. Most of the time conversion uses full
 delta and unification does no delta. This fine-grain is used in
 rewrite/setoid_rewrite, where only closed-term delta on global constants is
 allowed. - Interpret Hint Unfold as a directive for delta conversion in
 auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints). -
 Remove ad-hoc support for this in typeclasses. Now setoid_rewrite works
 correctly w.r.t. the old version regarding local definitions. - Fix closed
 bugs which needed updating due to syntax modifications.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10824 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenvtac.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index c966e876f9..22dcca2890 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -96,10 +96,9 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft
 open Unification
 
 let fail_quick_unif_flags = {
-  modulo_conv_on_closed_terms = true; 
+  modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = false;
-  modulo_delta = Cpred.empty; 
-  modulo_zeta = true;
+  modulo_delta = empty_transparent_state;
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-- 
cgit v1.2.3