From 07a6858653428d4142583ca8feec8f57d6064de0 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Mon, 13 Oct 2003 13:12:05 +0000
Subject: Ground update changing left-arrow-arrow rule.

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

diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index bd69262906..b047e01f16 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -153,9 +153,10 @@ let ll_arrow_tac a b c backtrack id continue seq=
             [exact_no_check (constr_of_reference id); 
 	     tclTHENLIST 
 	       [generalize [d];
-		introf;
 		clear_global id;
-		tclCOMPLETE (wrap 1 true continue seq)]]])
+		introf;
+		introf;
+		tclCOMPLETE (wrap 2 true continue seq)]]])
       backtrack
 
 (* quantifier rules (easy side) *)
-- 
cgit v1.2.3