From 16d21ec245179d2a735ec71e96d7c356f023521c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 7 Nov 2017 01:55:26 -0500 Subject: Split off computational part of basesystem_partial_evaluation_RHS_gen --- src/Arithmetic/Core.v | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'src/Arithmetic') diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index cfcc71e65..f3692c86d 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -1216,13 +1216,17 @@ Ltac apply_patterned_full t1 := (@ModularArithmetic.F.to_Z) (@ModularArithmetic.F.of_Z) 2%Z 1%Z 0%Z). -Ltac basesystem_partial_evaluation_RHS_gen unfold_tac := - let t := match goal with |- _ _ ?t => t end in +Ltac basesystem_partial_evaluation_gen unfold_tac t t1 := let t := unfold_tac t in let t := pattern_strip t in - let t1 := fresh "t1" in - pose t as t1; + let dummy := match goal with _ => pose t as t1 end in let t1' := apply_patterned t1 in + t1'. + +Ltac basesystem_partial_evaluation_RHS_gen unfold_tac := + let t := match goal with |- _ _ ?t => t end in + let t1 := fresh "t1" in + let t1' := basesystem_partial_evaluation_gen unfold_tac t t1 in transitivity t1'; [replace_with_vm_compute t1; clear t1|reflexivity]. @@ -1231,6 +1235,8 @@ Ltac basesystem_partial_evaluation_default_unfolder t := Ltac basesystem_partial_evaluation_RHS := basesystem_partial_evaluation_RHS_gen basesystem_partial_evaluation_default_unfolder. +Ltac basesystem_partial_evaluation := + basesystem_partial_evaluation_gen basesystem_partial_evaluation_default_unfolder. (** This block of tactic code works around bug #5434 -- cgit v1.2.3