[dev] Add include versions for Dune builds.

2019-02-18T17:15:44+00:00

Fixes #9537

This way, users can do:
```
dune exec coqtop.byte
> Drop.
 # #directory "dev";;
 # #use "include_dune";;
```

Separate variance and universe fields in inductives.

2019-02-17T14:44:30+00:00

I think the usage looks cleaner this way.

Cleanup debug printers a bit, add generated mli.

2017-12-22T15:36:32+00:00

Adding econstr printer to "include" file.

2017-07-12T15:28:43+00:00

Fix a bug in cumulativity

2017-06-16T02:52:11+00:00

Clean up universes of constants and inductives

2017-06-16T02:51:19+00:00

Squashed commit of the following:

2017-06-16T02:51:16+00:00

Except I have disabled the minimization of universes after sections as
it seems to interfere with the STM machinery causing files like
test-suite/vio/print.v to loop when processed asynchronously.

This is very peculiar and needs more investigation as the aforementioned
file does not have any sections or any universe polymorphic definitions!

commit fc785326080b9451eb4700b16ccd3f7df214e0ed
Author: Amin Timany 
Date:   Mon Apr 24 17:14:21 2017 +0200

    Revert STL to monomorphic

commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996
Author: Amin Timany 
Date:   Mon Apr 24 17:02:42 2017 +0200

    Try unifying universes before apply subtyping

commit ff393742c37b9241c83498e84c2274967a1a58dc
Author: Amin Timany 
Date:   Sun Apr 23 13:49:04 2017 +0200

    Compile more of STL with universe polymorphism

commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6
Author: Amin Timany 
Date:   Tue Apr 18 21:26:45 2017 +0200

    Made more progress on compiling the standard library

commit b8550ffcce0861794116eb3b12b84e1158c2b4f8
Author: Amin Timany 
Date:   Sun Apr 16 22:55:19 2017 +0200

    Make more number theoretic modules monomorphic

commit 29d126d4d4910683f7e6aada2a25209151e41b10
Author: Amin Timany 
Date:   Fri Apr 14 16:11:48 2017 +0200

    WIP more of standard library compiles

    Also: Matthieu fixed a bug in rewrite system which was faulty when
    introducing new morphisms (Add Morphism) command.

commit 23bc33b843f098acaba4c63c71c68f79c4641f8c
Author: Amin Timany 
Date:   Fri Apr 14 11:39:21 2017 +0200

    WIP: more of the standard library compiles

    We have implemented convertibility of constructors up-to mutual
    subtyping of their corresponding inductive types. This is similar to
    the behavior of template polymorphism.

commit d0abc5c50d593404fb41b98d588c3843382afd4f
Author: Amin Timany 
Date:   Wed Apr 12 19:02:39 2017 +0200

    WIP: trying to get the standard library compile with universe polymorphism

    We are trying to prune universes after section ends. Sections add a
    load of universes that are not appearing in the body, type or the
    constraints.

Adding a printer for Proof.proof reflecting the focusing layout.

2017-01-26T17:39:41+00:00

This is a modest contribution serving before all the purpose of
displaying the focus stack and the shelf and give_up list. It does not
print the sigma (while it could).

Any improvements are welcome.

FIX: dev/include

2016-11-05T15:28:23+00:00

A fix to dev/include.

2016-08-17T08:32:47+00:00

coq/dev/include, branch master