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
---
 plugins/decl_mode/decl_proof_instr.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c5fcabfc3b..ad315035ad 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -328,7 +328,7 @@ let enstack_subsubgoals env se stack gls=
 		meta_aux se.se_last_meta [] (List.rev rc) in
 	    let refiner = applist (appterm,List.rev holes) in
 	    let evd = meta_assign se.se_meta
-              (refiner,(ConvUpToEta 0,TypeProcessed (* ? *))) se.se_evd in
+              (refiner,(Conv,TypeProcessed (* ? *))) se.se_evd in
 	    let ncreated = replace_in_list
 	      se.se_meta nmetas se.se_meta_list in
 	    let evd0 = List.fold_left
@@ -375,7 +375,7 @@ let find_subsubgoal c ctyp skip submetas gls =
 	  if n <= 0 then
 	      {se with
 		 se_evd=meta_assign se.se_meta
-                  (c,(ConvUpToEta 0,TypeNotProcessed (* ?? *))) unifier;
+                  (c,(Conv,TypeNotProcessed (* ?? *))) unifier;
 	         se_meta_list=replace_in_list
 		  se.se_meta submetas se.se_meta_list}
 	  else
-- 
cgit v1.2.3