diff options
author | 2016-04-13 14:38:26 +0200 | |
---|---|---|
committer | 2016-04-27 21:55:48 +0200 | |
commit | 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a (patch) | |
tree | 4bf6607f8a29238bac0d87775d74f2105a1b9384 /theories/MSets/MSetList.v | |
parent | 8c74d3e5578caeb5c62ba462528d9972c1de17f1 (diff) |
Temporary hack to compensate missing comma while re-printing tactic
"exists c1, c2".
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 fb0d1ad9d..4c0ce86b4 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', s3'. + exists s1'; exists 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', s3'; do 2 (split; trivial). + exists s1'; exists 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', s3'; do 2 (split; trivial). + exists s1'; exists 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, s'; repeat split; auto using @ok. - exists s', s; repeat split; auto using @ok. + exists s; exists s'; repeat split; auto using @ok. + exists s'; exists s; repeat split; auto using @ok. Qed. End MakeRaw. |