coq/test-suite/misc/poly-capture-global-univs/src, branch master The formal proof system [test-suite] Fix evil plugin after changes in declare API. 2019-07-02T14:12:16+00:00 Emilio Jesus Gallego Arias 2019-06-25T23:00:32+00:00 5d20cce67d63bcf08458e3c4803257867f39b88a We should have this in the check target, but meanwhile we have to do manual housekeeping here. 
We should have this in the check target, but meanwhile we have to do
manual housekeeping here.
Duplicate the type of constant entries in Proof_global. 2019-06-24T09:02:11+00:00 Pierre-Marie Pédrot 2019-06-16T17:09:25+00:00 f597952e1b216ca5adf9f782c736f4cfe705ef02 This allows to desynchronize the kernel-facing API from the proof-facing one. 
This allows to desynchronize the kernel-facing API from the proof-facing one.
Add relevance marks on binders. 2019-03-14T12:27:38+00:00 Gaëtan Gilbert 2017-10-31T16:04:02+00:00 23f84f37c674a07e925925b7e0d50d7ee8414093 Kernel should be mostly correct, higher levels do random stuff at times. 
Kernel should be mostly correct, higher levels do random stuff at
times.
Separate variance and universe fields in inductives. 2019-02-17T14:44:30+00:00 Gaëtan Gilbert 2019-01-30T13:39:28+00:00 a9f0fd89cf3bb4b728eb451572a96f8599211380 I think the usage looks cleaner this way. 
I think the usage looks cleaner this way.
Use arrays of names instead of lists in abstract universe names. 2018-11-09T13:10:27+00:00 Pierre-Marie Pédrot 2018-10-01T11:40:45+00:00 23ef45aa14308aa0b1e1b1f6061ec9e7e7634e49 There is little point in having a list, as there is virtually no sharing nor expansion of bound universe names. This representation is thus more compact. 
There is little point in having a list, as there is virtually no sharing
nor expansion of bound universe names. This representation is thus more
compact.
Adding universe names to polymorphic entry instances. 2018-11-09T13:10:27+00:00 Pierre-Marie Pédrot 2018-09-27T12:23:25+00:00 601ce3738253e4bb197900ee6dad271c4e3666d6 






Porting the test-suite to coqpp.
2018-10-19T14:24:46+00:00

Pierre-Marie Pédrot

2018-10-19T14:21:22+00:00

266050f7aaa0ee0b090b30b1acabaccda6919889












Add test for inconsistency from polymorphism capturing global univs
2018-09-13T13:05:57+00:00

Gaëtan Gilbert

2018-08-28T14:11:17+00:00

eb4171d50d340e19e87a7a592b3d9c0d48654337