diff options
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 = *) |