From f55e532771a3aeddeb7d6fdad6247572af936b5b Mon Sep 17 00:00:00 2001
From: delahaye
Date: Wed, 3 May 2000 22:32:32 +0000
Subject: Completion d'un match non exhaustif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@411 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_trees.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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); 
-- 
cgit v1.2.3