The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 08/17/2018 04:36 PM, Kevin Hamlen wrote:
> What do Coq programmers consider the "right way" to organize large 
> projects containing functors?  In particular, how do authors of large 
> projects define collections of modules that all build upon some shared 
> functor without getting duplicate name-conflicts?

It really seems like a distraction to work so hard to put an inductive 
definition directly inside a functor body.  I would do it like this:

Module Type FOO_TYPE.
  Parameter foo: Type.
End FOO_TYPE.

Inductive bar T := Bar (f : T).

Module FooDefs (Foo: FOO_TYPE).
  Definition bar := bar Foo.foo.
  (* ... hundreds more definitions ... *)
End FooDefs.

Module FooTheory1 (Foo: FOO_TYPE).
  Module Import F := FooDefs Foo.
  Ltac silly1 := match goal with |- Bar _ _ = Bar _ _ => reflexivity end.
  (* ... more theorems, proofs, and ltacs ... *)
End FooTheory1.

Module Foo:FOO_TYPE.
  Definition foo:=nat.
End Foo.
Module Import FD := FooDefs Foo.
Module Import FT1 := FooTheory1 Foo.
Theorem silly: forall (x:bar), x=x.
Proof.
  destruct x.
  silly1.
Qed.