diff options
| author | Jasper Hugunin | 2020-08-25 13:07:08 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:32 -0700 |
| commit | 2d01a4794e4a684d9868ab7e7e58966a12161de7 (patch) | |
| tree | 34f8b6bac1830f3eee3291fae516555d7f8b7737 /theories/Structures | |
| parent | 17ed93c2caadfcf3a2aee8f2b9683191063b2951 (diff) | |
Modify Structures/OrdersTac.v to compile with -mangle-names
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/OrdersTac.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 408348139d..1c8073972d 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -100,9 +100,9 @@ Definition interp_ord o := match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end. Local Notation "#" := interp_ord. -Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. +Lemma trans o o' x y z : #o x y -> #o' y z -> #(o+o') x z. Proof. -destruct o, o'; simpl; intros x y z; +destruct o, o'; simpl; rewrite ?P.le_lteq; intuition auto; subst_eqns; eauto using (StrictOrder_Transitive x y z) with *. Qed. |