From be299971b29dbed7837c497fd59c192e4d0add72 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 4 May 2011 17:28:47 +0000
Subject: First phase removing obsolete support for eta up to conversion in
 "apply" unification. Assuming w_unify_0 is not eventually abandoned, it
 remains to merge unify_with_eta into unify_0 (what unify_with_eta does and
 that unify_0 does not do is to select of two instances of the same meta the
 one with less lambda's; it is unclear whether this is useful heuristic).

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

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 687bf32c62..632bf3a62d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -183,7 +183,7 @@ let clenv_assign mv rhs clenv =
       else
 	clenv
     else
-      let st = (ConvUpToEta 0,TypeNotProcessed) in
+      let st = (Conv,TypeNotProcessed) in
       {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
   with Not_found ->
     error "clenv_assign: undefined meta"
@@ -439,7 +439,7 @@ let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
-  { clenv' with evd = meta_assign k (c,(UserGiven,status)) clenv'.evd }
+  { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
 
 let clenv_match_args bl clenv =
   if bl = [] then
-- 
cgit v1.2.3