| Commit message (Expand) | Author | Age |
* | Update headers following #6543. | Théo Zimmermann | 2018-02-27 |
* | Bump year in headers. | Pierre-Marie Pédrot | 2017-07-04 |
* | Chasing a few unsafe constr coercions. | Pierre-Marie Pédrot | 2017-02-14 |
* | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | Ensuring purity of datastructures in the API. | Pierre-Marie Pédrot | 2015-04-16 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | In discrimination nets, do not index lambdas if they're part of a beta | Matthieu Sozeau | 2014-12-12 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Fix discrimination net which was not recognizing primitive projections. | Matthieu Sozeau | 2014-07-30 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Term dnets do no need to contain the afferent constr pattern in their nodes. | Pierre-Marie Pédrot | 2014-03-03 |
* | Removing Termdn, and putting the relevant code in Btermdn. The current Termdn | Pierre-Marie Pédrot | 2014-03-03 |
* | Extruding code not depending of the functor argument in Termdn. | Pierre-Marie Pédrot | 2014-03-03 |
* | Removing Pervasives.compare in Termdn. | Pierre-Marie Pédrot | 2014-02-28 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Monomorphization (tactics) | ppedrot | 2012-11-25 |
* | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot | 2012-11-08 |
* | This patch removes unused "open" (automatically generated from | regisgia | 2012-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey | 2012-05-29 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Fix discrimination of sorts which doesn't play well with cumulativity | msozeau | 2010-05-02 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Backport fix for indexing of sorts which collapse every Type occurrence | msozeau | 2009-10-28 |
* | This big commit addresses two problems: | soubiran | 2009-10-21 |
* | Better use of transparency information for local hypotheses: | msozeau | 2009-09-22 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Fix bug in term dnet preventing some unifications. Allow "higher-order" | msozeau | 2008-07-28 |
* | Enhanced discrimination nets implementation, which can now work with | msozeau | 2008-06-27 |
* | The type Pattern.constr_label was isomorphic to Libnames.global_reference. | sacerdot | 2004-12-07 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | entetes | filliatr | 2001-03-15 |
* | Déplacement du type reference dans Term | herbelin | 2000-04-28 |
* | Introduction d'un type constr_pattern pour les différents filtrages | herbelin | 2000-04-26 |
* | Nettoyage | herbelin | 2000-04-26 |
* | discriminations nets | filliatr | 1999-11-19 |