diff options
| author | Jasper Hugunin | 2020-08-24 15:58:23 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:31 -0700 |
| commit | a66a9cdfe02409a5d3fd1dcad47b9c6932a0d061 (patch) | |
| tree | b8390a51a4d3a52abf97d4f4f7a354f213cf9671 | |
| parent | 25d1767bd378d555f3cbcda303639d7a4604c759 (diff) | |
Modify Classes/CMorphisms.v to compile with -mangle-names
| -rw-r--r-- | theories/Classes/CMorphisms.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 598bd8b9c5..9a3a1d3709 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -20,7 +20,7 @@ Require Import Coq.Program.Tactics. Require Export Coq.Classes.CRelationClasses. Generalizable Variables A eqA B C D R RA RB RC m f x y. -Local Obligation Tactic := simpl_crelation. +Local Obligation Tactic := try solve [ simpl_crelation ]. Set Universe Polymorphism. @@ -268,6 +268,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H B R' H0 x y z X X0 x0 y0 X1. assert(R x0 x0). - transitivity y0... symmetry... - transitivity (y x0)... @@ -284,6 +285,7 @@ Section GenericInstances. Next Obligation. Proof. + intros A B C RA RB RC f mor x y X x0 y0 X0. apply mor ; auto. Qed. @@ -297,6 +299,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x y X x0 y0 X0 X1. transitivity x... transitivity x0... Qed. @@ -309,6 +312,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x x0 y X X0. transitivity y... Qed. @@ -318,6 +322,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x x0 y X X0. transitivity x0... Qed. @@ -327,6 +332,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x x0 y X X0. transitivity y... symmetry... Qed. @@ -335,6 +341,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x x0 y X X0. transitivity x0... symmetry... Qed. @@ -343,6 +350,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x x0 y X. split. - intros ; transitivity x0... - intros. @@ -358,6 +366,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x y X y0 y1 e X0; destruct e. transitivity y... Qed. @@ -368,6 +377,7 @@ Section GenericInstances. Next Obligation. Proof with auto. + intros A R H x y X x0 y0 X0. split ; intros. - transitivity x0... transitivity x... symmetry... |