From fdbc16dff05e57389a17a360814011f40489b499 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 22 Feb 2002 09:56:54 +0000
Subject: suppression de pop_named meilleure discrimination dans les tactiques
 d'inversion

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

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 85c0a02978..cf6df42ce9 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -748,7 +748,7 @@ let pr_prim_rule = function
   | {name=Intro_after;newids=[id]} -> 
       str"intro after "  ++ pr_id id
 	
-  | {name=Intro_replacing;newids=[id]} -> 
+  | {name=Intro_replacing;hypspecs=[id]} -> 
       (str"intro replacing "  ++ pr_id id)
 	
   | {name=Cut b;terms=[t];newids=[id]} ->
-- 
cgit v1.2.3