diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-24 17:07:43 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-24 17:08:11 -0400 |
| commit | fb6fd35b9cfc454b622c8bfa1364efdbf048e0df (patch) | |
| tree | f3915167b80db7c1a3052fe978a917fc9a0107bd /src/ModularArithmetic/ModularBaseSystemOpt.v | |
| parent | 399d059f701807158458cc67928993e56846444a (diff) | |
Work around lack of Fixpoint 'equation' lemmas in Coq < 8.4pl6
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index fd144a474..000f2599c 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -636,7 +636,8 @@ Global Instance Proper_fold_chain {T} {Teq} {Teq_Equivalence : Equivalence Teq} ==> Teq) fold_chain. Proof. do 9 intro. - subst; induction y1; repeat intro; rewrite !fold_chain_equation. + subst; induction y1; repeat intro; + unfold fold_chain; fold @fold_chain. + inversion H; assumption || reflexivity. + destruct a. apply IHy1. |