aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/global.ml
Commit message (Expand)AuthorAge
* selective join/export of the safe_environmentGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Less ocaml warnings.Gravatar Hugo Herbelin2014-06-13
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Safe_typing code refactoringGravatar letouzey2013-08-20
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* Simple machinery to detect EXTEND that interpret during parsingGravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Added a Register Inline command for the native compiler. Will be ported to th...Gravatar mdenes2013-07-10
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Minor simplifications in Declaremods and Safe_typingGravatar letouzey2013-04-15
* Mod_subst: misc reformulationsGravatar letouzey2013-02-26
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of LabelGravatar ppedrot2012-12-18
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Noise for nothingGravatar pboutill2012-03-02
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* Rely on kernel to know if a name is already used so as to be consistent with it.Gravatar herbelin2011-10-08
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Nouveau mécanisme pour les modules interactifs : les arguments deGravatar herbelin2006-04-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 21:19:58 +0000