Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Circular Dependencies

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Circular Dependencies


Chronological Thread 
  • From: "Jeffrey Terrell" <jeffrey.w.terrell AT gmail.com>
  • To: <coq-club AT inria.fr>
  • Subject: [Coq-Club] Circular Dependencies
  • Date: Wed, 30 May 2018 10:19:44 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jeffrey.w.terrell AT gmail.com; spf=Pass smtp.mailfrom=jeffrey.w.terrell AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f44.google.com
  • Ironport-phdr: 9a23:CJEC2xX3N5h2lCFePsEM0AFfxzvV8LGtZVwlr6E/grcLSJyIuqrYYxKAt8tkgFKBZ4jH8fUM07OQ7/i9HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9yIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kaxVrhGuqBNjxIDUfJqYO+BicqPSZd4WW3ZNUthXWidcAo28dYwPD+8ZMOpWq4fyuVUOrRWkBQayBOLk1yFGiWHs3a0gzeshFQXG0AI9FN8JsnTbstv1NKkIUe+rzKjE1zvCY+lK2Tjj8ojIaA4uofWIXb9rfsrRzFMgFwLBjlmKtYPlODaV2/0LvmOG7ORgTfqihmwopg1rvzSj2MchhpPKi44L0FzJ+ip0zJ41KNGiVUJ2YcKoHIFUui2ELYd6X80vT31utS0n0LMJo4S7czIPyJk/xx7QdfiHc4+Q7xLmTumRIDN4iGtrebK6mxq+6Eagx+LzW8Wu31ZKqS1FktbItn8TzRDc9s+HSv5l8keg3zaAyRzT5/lGLE07j6bXNoAtz74qmpcQr0jPBCD7lUrugK+TbEok++yo6+r9YrXho5+RL410hR/wMqQggMywH+Q5PhIAXmSB5eSzyqfj/VfnT7VOiv07iabZsJXAKsQaoq61GRNa0oEm6xqnFTepzMwYnWUbLFJCYB+Ik4/pO0jXLP/kCfe/nk+jnSxwx/HGO73hGo/CImLCkLfnZ7Z96lRTxBA9zdBFtNpoDeRVK/XqH0T1qdbwDxkjMgXyzfyxW/tn0YZLE0CCDKGDPbKajVKS/O8rJ6PEMI0YtjjnJulj+LjygGUjlFsZVaas1JoTLnu/G6I1cA2ifXPwj4JZQi8xtQ0kQbmy0QzQYXtof3+3GpkEyHQ+AYOiA53EQ9n00rOE1Sa/WJZRYzIfUwzeITLTb4yBHsw0RmeKOMY4y24LULGgT8kq0hT87FanmYoiFfLd/2gjjbym1NVx4LeOxxQ79DgxEMHFlm/REyd7mWQHQzJw16d68xRw

Hi,

 

I’m not surprised that  “make” dropped the dependency.

 

make: Circular B.vo <- A.vo dependency dropped

 

A.v :

Require Import B.

Module A.

Definition X : Prop := B.Y.

End A.

 

B.v :

Require Import A.

Module B.

Definition Y : Prop := A.X.

End B.

 

Is it possible to overcome this problem?

 

Regards,

Jeff.



  • [Coq-Club] Circular Dependencies, Jeffrey Terrell, 05/30/2018

Archive powered by MHonArc 2.6.18.

Top of Page