index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
univ.mli
Commit message (
Expand
)
Author
Age
...
*
- Fix hashing of levels to get the "right" order in universe contexts etc...
Matthieu Sozeau
2014-06-04
*
Find a more efficient fix for dealing with template universes:
Matthieu Sozeau
2014-05-06
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
- Fix handling of polymorphic inductive elimination schemes.
Matthieu Sozeau
2014-05-06
*
- Rename eq to equal in Univ, document new modules, set interfaces.
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Fixing Pervasives.equality in extraction.
Pierre-Marie Pédrot
2014-03-03
*
Specializing hash functions for widely used types.
ppedrot
2013-10-24
*
Universe counters on slaves are in sync with master
gareuselesinge
2013-08-20
*
A version of Univ.check_eq with no anomaly for Evd.set_eq_sort
letouzey
2013-03-12
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Modulification of dir_path
ppedrot
2012-12-14
*
Small cleaning of interface in Univ
ppedrot
2012-11-26
*
univ inconsistency error message gives evidence of a cycle
barras
2012-10-17
*
Updating headers.
herbelin
2012-08-08
*
Univ: enforce_leq instead of enforce_geq for more uniformity
letouzey
2012-03-22
*
Univ: a univ_depends function to avoid a hack in Inductiveops
letouzey
2012-03-01
*
When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty
letouzey
2011-10-26
*
Hash-consing of mutual_inductive_body (and Univ.constraints)
letouzey
2011-10-10
*
Hash-consing of constr could share more
letouzey
2011-10-02
*
Fix the hconsing of universes
letouzey
2011-09-07
*
Tentative to make unification check types at every instanciation of an
msozeau
2011-03-11
*
Add "Print Sorted Universes"
glondu
2011-01-11
*
More coherent comment ordering
glondu
2011-01-11
*
Univ.constraints made fully abstract instead of being a Set of abstract stuff
letouzey
2010-12-18
*
In Univ, unify order_request and constraint_type
glondu
2010-11-03
*
More generic Univ.dump_universes
glondu
2010-11-02
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Correction d'une incohérence de typage des inductifs polymorphes: les
herbelin
2008-07-25
*
ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...
soubiran
2008-06-06
*
Changement de stratégie vis à vis du commit 10859 sur la gestion des
herbelin
2008-05-12
*
Correction du bug des types singletons pas sous-type de Set
herbelin
2008-04-27
*
added the .vo checker (with independent Makefile)
barras
2008-04-21
*
Nettoyage de code en vue de la release. Plus de Warning: Unused
aspiwack
2007-12-18
*
Ajout infos de débogage de "universe inconsistency" quand option Set
herbelin
2007-09-30
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Prise en compte des univers algébriques dans les types inférés dans
herbelin
2007-01-19
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Inductifs avec polymorphisme de sorte (version initiale)
herbelin
2006-03-29
*
Code v7 obsolete
herbelin
2005-05-05
*
Nouvelle en-tête
herbelin
2004-07-16
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
GROS COMMIT:
barras
2001-11-05
*
Nettoyage des commentaires
herbelin
2001-09-20
*
Passage aux univers algébriques
herbelin
2001-09-09
[prev]
[next]