diff options
| author | letouzey | 2013-03-12 23:59:10 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-12 23:59:10 +0000 |
| commit | 0e7855095be6f06d1dcf563a9036b79e20172d28 (patch) | |
| tree | ef7e9de44d50b2b9e149629393946008506e0bc7 /plugins | |
| parent | 6d5eee245a85f410ec184353ab9f38ce3aa4e331 (diff) | |
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
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 = *) |