From 1fe616bda25a6208c4d19f61220e570c71bcc25a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 7 Dec 2004 08:25:12 +0000 Subject: [PATCH] symmetry of equality NOT used in auto --- helm/ocaml/metadata/metadataConstraints.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 28973af97..2c04562d8 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -407,7 +407,7 @@ let myspeciallist_of_facts = [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"] let myspeciallist = [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; - 0,"cic:/Coq/Init/Logic/sym_eq.con"; +(* 0,"cic:/Coq/Init/Logic/sym_eq.con"; *) 0,"cic:/Coq/Init/Logic/trans_eq.con"; 0,"cic:/Coq/Init/Logic/f_equal.con"; 0,"cic:/Coq/Init/Logic/f_equal2.con"; -- 2.39.2