From 9b3b1a9d73cac7ef55fc0744650eb0f668cb98a8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 27 Mar 2002 20:29:20 +0000
Subject: Simplification de Proof_type.prim_rule

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index b369bbf311..9a5f803d3c 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -167,7 +167,7 @@ let rule_to_ntactic r =
      (match r with
        Tactic (s,l) ->
 	 Ast.ope (s,(List.map ast_of_cvt_arg l))
-     | Prim {name=Refine;hypspecs=_; newids=_; params=_; terms=[h]} ->
+     | Prim (Refine h) ->
 	 Ast.ope ("Exact",
 		  [Node ((0,0), "COMMAND", [ast_of_constr h])])
      | _ -> Ast.ope ("Intros",[])) in
-- 
cgit v1.2.3