diff options
| author | herbelin | 2002-03-27 20:29:20 +0000 |
|---|---|---|
| committer | herbelin | 2002-03-27 20:29:20 +0000 |
| commit | 9b3b1a9d73cac7ef55fc0744650eb0f668cb98a8 (patch) | |
| tree | df1da379e59f5b59df8b5d61d6c0151b69929751 /contrib/interface | |
| parent | 93bd05ce0dc68892375a77df0d4ac7d73770c433 (diff) | |
Simplification de Proof_type.prim_rule
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2571 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/showproof.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |