diff options
| author | letouzey | 2013-03-13 00:00:12 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-13 00:00:12 +0000 |
| commit | 552df1605233769ad3cdabaadaa0011605e79797 (patch) | |
| tree | 28c3ae6a250aba80e1eb53ff9d906df9f49b75c1 /plugins/funind/functional_principles_proofs.ml | |
| parent | da3cbbcef1f4de9780603225e095f026bb5da709 (diff) | |
Restrict (try...with...) to avoid catching critical exn (part 7)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16283 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index a5e7d6c4d1..f8ea1d528f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1224,7 +1224,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let ctxt,pte_app = (decompose_prod_assum (pf_concl gl)) in let pte,pte_args = (decompose_app pte_app) in try - let pte = try destVar pte with _ -> anomaly (Pp.str "Property is not a variable") in + let pte = + try destVar pte + with DestKO -> anomaly (Pp.str "Property is not a variable") + in let fix_info = Id.Map.find pte ptes_to_fix in let nb_args = fix_info.nb_realargs in tclTHENSEQ |