diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 0714c93b..13b7fb40 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -1251,13 +1251,18 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV +let report_anomaly _ = + let e = UserError ("", Pp.str "Conversion test raised an anomaly") in + let e = Errors.push e in + iraise e + let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = try let evars ev = safe_evar_value sigma ev in let _ = f ~evars reds env (Evd.universes sigma) x y in true with Reduction.NotConvertible -> false - | e when is_anomaly e -> error "Conversion test raised an anomaly" + | e when is_anomaly e -> report_anomaly e let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv_universes reds env sigma let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq_universes reds env sigma @@ -1275,7 +1280,7 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true with Reduction.NotConvertible -> false | Univ.UniverseInconsistency _ -> false - | e when is_anomaly e -> error "Conversion test raised an anomaly" + | e when is_anomaly e -> report_anomaly e let sigma_compare_sorts env pb s0 s1 sigma = match pb with @@ -1316,7 +1321,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) with | Reduction.NotConvertible -> sigma, false | Univ.UniverseInconsistency _ when catch_incon -> sigma, false - | e when is_anomaly e -> error "Conversion test raised an anomaly" + | e when is_anomaly e -> report_anomaly e let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> Reduction.generic_conv pb ~l2r (safe_evar_value sigma)) @@ -1646,7 +1651,7 @@ let betazetaevar_applist sigma n c l = if Int.equal n 0 then applist (substl env t, stack) else match kind_of_term t, stack with | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack + | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | Evar ev, _ -> (match safe_evar_value sigma ev with | Some body -> stacklam n env body stack |