diff options
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 |