From c4a45cc04f9c350c38b148a85bed0c7e88ca5afc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 24 Dec 2002 11:28:22 +0000
Subject: Utilisation du second-ordre avec possibilité de K-rédex dans lemInv

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

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index fcc1884caf..0e337a0c8f 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -291,7 +291,7 @@ let lemInv id c gls =
     let (wc,kONT) = startWalk gls in
     let clause = mk_clenv_type_of wc c in
     let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in
-    res_pf kONT clause gls
+    elim_res_pf kONT clause true gls
   with 
 (* Ce n'est pas l'endroit pour cela
     | Not_found  ->  
-- 
cgit v1.2.3