From 86002ce6e6fb3cbf1f5c9bf3657c13b4e79be192 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 20 Sep 2010 21:59:57 +0000
Subject: Added eta-expansion in kernel, type inference and tactic unification,
 governed in the latter case by a flag since (useful e.g. for setoid rewriting
 which otherwise loops as it is implemented).

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

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 85e4580c86..90c2335d68 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -107,6 +107,7 @@ let fail_quick_unif_flags = {
   modulo_delta = empty_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = false;
+  modulo_eta = true
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-- 
cgit v1.2.3