diff options
Diffstat (limited to 'src/Arithmetic')
-rw-r--r-- | src/Arithmetic/Core.v | 14 |
1 files changed, 10 insertions, 4 deletions
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 |