diff options
| author | Maxime Dénès | 2018-09-11 13:14:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-11 13:14:46 +0200 |
| commit | 664ceaa604b67e8b4d1638b5df0adafbdd2c1807 (patch) | |
| tree | b314c502ad3ffe12b2ae6f36b88037a6d09b29a6 /plugins/ssr | |
| parent | 2f0e274a1436b477e0be0be94a36ee9461a89767 (diff) | |
| parent | 03bb8c6a22fea0214179e6d5a9d97327d548d2fd (diff) | |
Merge PR #8284: [ssr] anomaly -> error
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 3 |
2 files changed, 6 insertions, 3 deletions
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index fbe3b000fb..602fcfcab5 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -293,7 +293,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let c, cl, ucst = match_pat env p occ h cl in let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in - let gl = try pf_unify_HO gl inf_t c with _ -> error gl c inf_t in + let gl = try pf_unify_HO gl inf_t c + with exn when CErrors.noncritical exn -> error gl c inf_t in cl, gl, post with | NoMatch | NoProgress -> @@ -302,7 +303,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let e = EConstr.of_constr e in let n, e, _, _ucst = pf_abs_evars gl (fst p, e) in let e, _, _, gl = pf_saturate ~beta:true gl e n in - let gl = try pf_unify_HO gl inf_t e with _ -> error gl e inf_t in + let gl = try pf_unify_HO gl inf_t e + with exn when CErrors.noncritical exn -> error gl e inf_t in cl, gl, post in let rec match_all concl gl patterns = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 23cbf49c05..f23433f2f4 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -115,7 +115,8 @@ let newssrcongrtac arg ist gl = (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = - match try Some (pf_unify_HO gl_c (pf_concl gl) c) with _ -> None with + match try Some (pf_unify_HO gl_c (pf_concl gl) c) + with exn when CErrors.noncritical exn -> None with | Some gl_c -> tclTHEN (Proofview.V82.of_tactic (convert_concl (fs gl_c c))) (t_ok (proj gl_c)) gl |