diff options
| -rw-r--r-- | proofs/proof_trees.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 446d4b2a29..e6150fba66 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -361,7 +361,8 @@ let ast_of_cvt_arg = function List.map (ast_of_cvt_bind (ast_of_constr false (assumptions_for_print []))) bl) - | Tacexp ast -> ope ("TACTIC",[ast]) + | Tacexp ast -> ope ("TACTIC",[ast]) + | Tac tac -> failwith "TODO: ast_of_cvt_arg: Tac" | Redexp red -> failwith "TODO: ast_of_cvt_arg: Redexp" | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); (num n); |