From 10caf1cda152590dd1f32d87e902ecac57d7d527 Mon Sep 17 00:00:00 2001 From: Andrew Appel Date: Wed, 20 Mar 2024 10:59:41 -0400 Subject: [PATCH] Adapt to Coq 8.19 and the flocq/interval packages that go with it --- vcfloat/Prune.v | 14 ++++++++------ vcfloat/compute_tactics_ltac2.v | 15 +++++++++++---- 2 files changed, 19 insertions(+), 10 deletions(-) diff --git a/vcfloat/Prune.v b/vcfloat/Prune.v index 88f914e..1a22cf6 100644 --- a/vcfloat/Prune.v +++ b/vcfloat/Prune.v @@ -1172,12 +1172,14 @@ apply (bconstexpr_correct' _ _ _ x vars Heqf H0). apply Rabs_pos. eassumption. eassumption. destruct (F.mul_UP_correct p52 t t0). left. split. - split. apply F'.valid_ub_real; auto. - unfold F.toR in H5. rewrite F.real_correct in H4. destruct (F.toX t); try discriminate. - simpl in H5. pose proof (Rabs_pos (eval e1 vars)); lra. - split. apply F'.valid_ub_real; auto. - unfold F.toR in H7. rewrite F.real_correct in H6. destruct (F.toX t0); try discriminate. - simpl in H7. pose proof (Rabs_pos (eval e2 vars)); lra. + clear - H4 H5. + rewrite F.real_correct in H4. unfold F.is_non_neg'. unfold F.toR in H5. + destruct (F.toX t); try discriminate. simpl in H5. + pose proof (Rabs_pos (eval e1 vars)). lra. + clear - H6 H7. + rewrite F.real_correct in H6. unfold F.is_non_neg'. unfold F.toR in H7. + destruct (F.toX t0); try discriminate. simpl in H7. + pose proof (Rabs_pos (eval e2 vars)). lra. unfold Xbind2 in H1. red in H1. unfold F.toR. rewrite F.real_correct in H8. destruct (F.toX (F.mul_UP p52 t t0)); try discriminate. diff --git a/vcfloat/compute_tactics_ltac2.v b/vcfloat/compute_tactics_ltac2.v index 16d596c..21b46b0 100644 --- a/vcfloat/compute_tactics_ltac2.v +++ b/vcfloat/compute_tactics_ltac2.v @@ -76,7 +76,9 @@ Ltac2 redflags_full () := (* zeta: expand let expressions by substitution *) Std.rZeta := true; (* Symbols to expand or not to expand (depending on rDelta) *) - Std.rConst := [] + Std.rConst := []; + (* Just guessing that Norm is the right thing here: *) + Std.rStrength := Std.Norm }. (** ** Ltac2 functions for evaluation restricted reductions on a term *) @@ -131,11 +133,13 @@ Ltac2 rec eval_cbv_uao_lr (head : constr) (rf : Std.red_flags) (term : constr) : then (Constr.Unsafe.make (Constr.Unsafe.Cast value_r cast type), true) else (term, false) +(* Commented this out for Coq 8.19 | Constr.Unsafe.Proj projection value => let (value_r, value_m) := eval_cbv_uao_lr head rf value in if value_m then (Constr.Unsafe.make (Constr.Unsafe.Proj projection value_r), true) else (term, false) +*) | Constr.Unsafe.Case case_a constr_return case_b constr_match case_funcs => let (match_r, match_m) := eval_cbv_uao_lr head rf constr_match in @@ -190,18 +194,21 @@ Ltac2 rec eval_cbv_uao_afr (head : constr) (rf : Std.red_flags) (term : constr) then (Constr.Unsafe.make (Constr.Unsafe.Cast value_r cast type_r), true) else (term, false) + +(* Commented this out for Coq 8.19 | Constr.Unsafe.Proj projection value => let (value_r, value_m) := eval_cbv_uao_afr head rf value in if value_m then (Constr.Unsafe.make (Constr.Unsafe.Proj projection value_r), true) else (term, false) - - | Constr.Unsafe.Case case_a constr_return case_b constr_match case_funcs => +*) + | Constr.Unsafe.Case case_a constr_return_rel case_b constr_match case_funcs => + let (constr_return, relev) := constr_return_rel in let (return_r, return_m) := eval_cbv_uao_afr head rf constr_return in let (match_r, match_m) := eval_cbv_uao_afr head rf constr_match in let case_funcs_e := Array.map (eval_cbv_uao_afr head rf) case_funcs in if return_m || match_m || (Array.exist pair_second case_funcs_e) - then (Constr.Unsafe.make (Constr.Unsafe.Case case_a return_r case_b match_r (Array.map pair_first case_funcs_e)), true) + then (Constr.Unsafe.make (Constr.Unsafe.Case case_a (return_r,relev) case_b match_r (Array.map pair_first case_funcs_e)), true) else (term, false) | Constr.Unsafe.Fix int_arr int binder_arr constr_arr =>