Resolving circular dependency error, adding not_symmetry to stdpp_tac…

…tics.v

stdpp/stdpp_tactics.v

@@ -1,9 +1,10 @@
-Require Import
-  MathClasses.misc.util.
 From Coq Require Export RelationClasses Relation_Definitions Lia.
 
 Module FastDoneTactic.
 
+Lemma not_symmetry {A} `{R : relation A, !Symmetric R} x y : ~ R x y -> ~ R y x.
+Proof. intuition. Qed.
+
 Ltac fast_done :=
   solve
     [ eassumption
@@ -15,23 +16,21 @@ Tactic Notation "fast_by" tactic(tac) :=
 
 End FastDoneTactic.
 
-Section DoneSection.
-  Import FastDoneTactic.
+Import FastDoneTactic.
 
-  Ltac done :=
-    solve
-    [ repeat first
-      [ fast_done
-      | solve [trivial]
-      (* All the tactics below will introduce themselves anyway, or make no sense
-         for goals of product type. So this is a good place for us to do it. *)
-      | progress intros
-      | solve [symmetry; trivial]
-      | solve [apply not_symmetry; trivial]
-      | discriminate
-      | contradiction
-      | split
-      | match goal with H : ~ _ |- _ => case H; clear H; fast_done end ]
-    ].
+Ltac done :=
+  solve
+  [ repeat first
+    [ fast_done
+    | solve [trivial]
+    (* All the tactics below will introduce themselves anyway, or make no sense
+       for goals of product type. So this is a good place for us to do it. *)
+    | progress intros
+    | solve [symmetry; trivial]
+    | solve [apply not_symmetry; trivial]
+    | discriminate
+    | contradiction
+    | split
+    | match goal with H : ~ _ |- _ => case H; clear H; fast_done end ]
+  ].
 
-End DoneSection.

time-of-build.log

@@ -0,0 +1,58 @@
+COQC ./misc/util.v
+File "./misc/util.v", line 1, characters 0-149:
+Warning: Notation "_ = _" was already used in scope type_scope.
+[notation-overridden,parsing,default]
+File "./misc/util.v", line 1, characters 0-149:
+Warning: Notation "_ ≠ _" was already used in scope type_scope.
+[notation-overridden,parsing,default]
+misc/util.vo (real: 5.25, user: 0.00, sys: 0.01, mem: 4896 ko)
+COQC ./misc/decision.v
+File "./misc/decision.v", line 1, characters 0-78:
+Warning: Notation "_ = _" was already used in scope type_scope.
+[notation-overridden,parsing,default]
+File "./misc/decision.v", line 1, characters 0-78:
+Warning: Notation "_ ≠ _" was already used in scope type_scope.
+[notation-overridden,parsing,default]
+misc/decision.vo (real: 3.03, user: 0.00, sys: 0.03, mem: 4328 ko)
+COQC ./interfaces/abstract_algebra.v
+File "./interfaces/abstract_algebra.v", line 1, characters 0-192:
+Warning: Notation "_ = _" was already used in scope type_scope.
+[notation-overridden,parsing,default]
+File "./interfaces/abstract_algebra.v", line 1, characters 0-192:
+Warning: Notation "_ ≠ _" was already used in scope type_scope.
+[notation-overridden,parsing,default]
+File "./interfaces/abstract_algebra.v", line 50, characters 0-76:
+Warning: Adding and removing hints in the core database implicitly is
+deprecated. Please specify a hint database.
+[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
+interfaces/abstract_algebra.vo (real: 2.89, user: 0.00, sys: 0.03, mem: 4892 ko)
+COQC ./theory/products.v
+File "./theory/products.v", line 1, characters 0-57:
+Warning: Notation "_ = _" was already used in scope type_scope.
+[notation-overridden,parsing,default]
+File "./theory/products.v", line 1, characters 0-57:
+Warning: Notation "_ ≠ _" was already used in scope type_scope.
+[notation-overridden,parsing,default]
+File "./theory/products.v", line 19, characters 35-46:
+Error: No such goal.
+
+Command exited with non-zero status 1
+theory/products.vo (real: 2.53, user: 0.00, sys: 0.00, mem: 4896 ko)
+make[4]: *** [Makefile.coq:838: theory/products.vo] Error 1
+make[4]: *** [theory/products.vo] Deleting file 'theory/products.glob'
+make[3]: *** [Makefile.coq:409: all] Error 2
+COQC ./theory/products.v
+File "./theory/products.v", line 1, characters 0-57:
+Warning: Notation "_ = _" was already used in scope type_scope.
+[notation-overridden,parsing,default]
+File "./theory/products.v", line 1, characters 0-57:
+Warning: Notation "_ ≠ _" was already used in scope type_scope.
+[notation-overridden,parsing,default]
+File "./theory/products.v", line 19, characters 35-46:
+Error: No such goal.
+
+Command exited with non-zero status 1
+theory/products.vo (real: 2.10, user: 0.01, sys: 0.01, mem: 4908 ko)
+make[4]: *** [Makefile.coq:838: theory/products.vo] Error 1
+make[4]: *** [theory/products.vo] Deleting file 'theory/products.glob'
+make[3]: *** [Makefile.coq:409: all] Error 2