diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:03 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:03 +0200 |
commit | 18512ba12400e30858ae19e5ef69b9590b96de06 (patch) | |
tree | d85d73110a1eb95b8873375cee0bd35821996657 /theories/MSets/MSetList.v | |
parent | 3011cbfb224b3b2dfb72afd05094614b97a2128b (diff) |
Revert "Temporary hack to compensate missing comma while re-printing tactic"
This reverts commit 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a.
Diffstat (limited to 'theories/MSets/MSetList.v')
-rw-r--r-- | theories/MSets/MSetList.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index 4c0ce86b4..fb0d1ad9d 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -795,7 +795,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. apply (StrictOrder_Irreflexive s2); auto. intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12) (s2'' & s3' & B2' & B3 & E2' & E3 & L23). - exists s1'; exists s3'. + exists s1', s3'. repeat rewrite <- isok_iff in *. do 4 (split; trivial). assert (eqlistA X.eq s2' s2''). @@ -809,11 +809,11 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. intros s1 s2 E12 s3 s4 E34. split. intros (s1' & s3' & B1 & B3 & E1 & E3 & LT). - exists s1'; exists s3'; do 2 (split; trivial). + exists s1', s3'; do 2 (split; trivial). split. transitivity s1; auto. symmetry; auto. split; auto. transitivity s3; auto. symmetry; auto. intros (s1' & s3' & B1 & B3 & E1 & E3 & LT). - exists s1'; exists s3'; do 2 (split; trivial). + exists s1', s3'; do 2 (split; trivial). split. transitivity s2; auto. split; auto. transitivity s4; auto. Qed. @@ -829,8 +829,8 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. intros s s' Hs Hs'. destruct (compare_spec_aux s s'); constructor; auto. - exists s; exists s'; repeat split; auto using @ok. - exists s'; exists s; repeat split; auto using @ok. + exists s, s'; repeat split; auto using @ok. + exists s', s; repeat split; auto using @ok. Qed. End MakeRaw. |