diff options
| author | Jasper Hugunin | 2020-10-09 15:49:42 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-11 19:05:14 -0700 |
| commit | f136bcf5a067fcf1e38f48062ccde06875709e6a (patch) | |
| tree | a6cf7042f1d33a3c34ca52d345d4dbff92242a82 | |
| parent | 6b04433e6828112bfbd7914ca941912427f0e4ff (diff) | |
Modify setoid_ring/Ring.v to compile with -mangle-names
| -rw-r--r-- | theories/setoid_ring/Ring.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/setoid_ring/Ring.v b/theories/setoid_ring/Ring.v index a66037a956..25b79d1fb2 100644 --- a/theories/setoid_ring/Ring.v +++ b/theories/setoid_ring/Ring.v @@ -17,22 +17,22 @@ Require Export Ring_tac. Lemma BoolTheory : ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)). split; simpl. -destruct x; reflexivity. -destruct x; destruct y; reflexivity. -destruct x; destruct y; destruct z; reflexivity. +intros x; destruct x; reflexivity. +intros x y; destruct x; destruct y; reflexivity. +intros x y z; destruct x; destruct y; destruct z; reflexivity. reflexivity. -destruct x; destruct y; reflexivity. -destruct x; destruct y; reflexivity. -destruct x; destruct y; destruct z; reflexivity. +intros x y; destruct x; destruct y; reflexivity. +intros x y; destruct x; destruct y; reflexivity. +intros x y z; destruct x; destruct y; destruct z; reflexivity. reflexivity. -destruct x; reflexivity. +intros x; destruct x; reflexivity. Qed. Definition bool_eq (b1 b2:bool) := if b1 then b2 else negb b2. Lemma bool_eq_ok : forall b1 b2, bool_eq b1 b2 = true -> b1 = b2. -destruct b1; destruct b2; auto. +intros b1 b2; destruct b1; destruct b2; auto. Qed. Ltac bool_cst t := |