aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
Commit message (Expand)AuthorAge
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Use type nonrec in some functor arguments.Gravatar Gaëtan Gilbert2017-10-16
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A few typos.Gravatar Hugo Herbelin2017-06-04
* Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Revised behavior on ill-formed identifiers.Gravatar Hugo Herbelin2017-05-20
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* refactoring "Names.DirPath.is_empty" functionGravatar Matej Kosik2017-04-20
* refactoring "Names.DirPath.compare" functionGravatar Matej Kosik2017-04-20
* refactoring "Names.DirPath.equal" functionGravatar Matej Kosik2017-04-20
* Revert "refactoring: Names.DirPath.equal"Gravatar Matej Košík2017-04-10
* Revert "refactoring: Names.DirPath.compare"Gravatar Matej Košík2017-04-10
* Revert "refactoring: Names.DirPath.is_empty"Gravatar Matej Košík2017-04-10
* refactoring: Names.DirPath.is_emptyGravatar Matej Kosik2017-04-10
* refactoring: Names.DirPath.compareGravatar Matej Kosik2017-04-10
* refactoring: Names.DirPath.equalGravatar Matej Kosik2017-04-10
* [safe-string] Enable -safe-string !Gravatar Emilio Jesus Gallego Arias2017-03-14
* [safe_string] library/nameopsGravatar Emilio Jesus Gallego Arias2017-03-14
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\
| * Fix #5242 - Dubious unsilenceable warning on invalid identifierGravatar Maxime Dénès2016-12-02
* | COMMENT: Names.Cmap and Names.Cmap_envGravatar Matej Kosik2016-10-26
* | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | Changing the definition of the "Lib.variable.info" type to enable us to do mo...Gravatar Matej Kosik2016-08-24
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2016-03-22
* | ADD: Names.Name.is_{anonymous,name}Gravatar Matej Kosik2016-02-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Gravatar Matej Kosik2016-01-11
* | COMMENTS: added to the "Names" module.Gravatar Matej Kosik2015-12-18
* | Better debug printers for module paths.Gravatar Maxime Dénès2015-09-20
|/
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
* Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
* Followup of 9f81b58551.Gravatar Pierre-Marie Pédrot2015-07-30
* Fixing bug #4289 (hash-consing only user part of constant notGravatar Hugo Herbelin2015-07-30
* Display functions for primitive projections.Gravatar Maxime Dénès2015-07-02
* Fixing bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
* Fix (actually, properly implement :) hashconsing of projections,Gravatar Matthieu Sozeau2014-12-17
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 15:26:07 +0000