From 0e7855095be6f06d1dcf563a9036b79e20172d28 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 12 Mar 2013 23:59:10 +0000
Subject: Recdef: an anomaly isn't so anomalous, occurs in 1618.v

 For the moment, this anomaly is catched and ignore later,
 but that will changed soon.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16272 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/functional_principles_proofs.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3c92bb5bd6..a5e7d6c4d1 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1563,7 +1563,7 @@ let prove_principle_for_gen
   let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
-     | None -> anomaly (str "No tcc proof !!")
+     | None -> error "No tcc proof !!"
      | Some lemma -> lemma
   in
 (*   let rec list_diff del_list check_list = *)
-- 
cgit v1.2.3