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 | |
| parent | 3011cbfb224b3b2dfb72afd05094614b97a2128b (diff) | |
Revert "Temporary hack to compensate missing comma while re-printing tactic"
This reverts commit 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a.
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetGenTree.v | 12 | ||||
| -rw-r--r-- | theories/MSets/MSetList.v | 10 |
2 files changed, 11 insertions, 11 deletions
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 4f5b6cde4..154c2384c 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -983,7 +983,7 @@ Proof. apply (StrictOrder_Irreflexive (elements s2)); auto. intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12) (s2'' & s3' & B2' & B3 & E2' & E3 & L23). - exists s1'; exists s3'; do 4 (split; trivial). + exists s1', s3'; do 4 (split; trivial). assert (eqlistA X.eq (elements s2') (elements s2'')). apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto with *. rewrite <- eq_Leq. transitivity s2; auto. symmetry; auto. @@ -995,11 +995,11 @@ Instance lt_compat : Proper (eq==>eq==>iff) lt. 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. @@ -1079,8 +1079,8 @@ Proof. intros. destruct (compare_Cmp s1 s2); constructor. rewrite eq_Leq; auto. - intros; exists s1; exists s2; repeat split; auto. - intros; exists s2; exists s1; repeat split; auto. + intros; exists s1, s2; repeat split; auto. + intros; exists s2, s1; repeat split; auto. Qed. @@ -1144,4 +1144,4 @@ Proof. apply mindepth_cardinal. Qed. -End Props. +End Props.
\ No newline at end of file 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. |