diff options
| author | delahaye | 2000-05-03 22:32:32 +0000 |
|---|---|---|
| committer | delahaye | 2000-05-03 22:32:32 +0000 |
| commit | f55e532771a3aeddeb7d6fdad6247572af936b5b (patch) | |
| tree | d027529a25d2f070533fcf7e83a064fb39f305eb | |
| parent | 4f75c55c9e512f808a482fa385b98abbd00892df (diff) | |
Completion d'un match non exhaustif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@411 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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); |