aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declaremods.ml
Commit message (Expand)AuthorAge
* [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [lib] Remove obsolete state-management function add_frozen_stateGravatar Emilio Jesus Gallego Arias2017-06-12
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* LtacProf for Coq trunkGravatar Jason Gross2016-06-05
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.Gravatar Pierre-Marie Pédrot2016-05-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Fix bug #4292: Unexpected functor objects.Gravatar Pierre-Marie Pédrot2016-05-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | Leveraging GADTs to provide a better Dyn API.Gravatar Pierre-Marie Pédrot2015-12-05
|/
* Declaremods: replace two anomalies by user errors (fix #3974 and #3975)Gravatar Pierre Letouzey2015-10-25
* Native compiler: refactor code handling pre-computed values.Gravatar Maxime Dénès2015-07-10
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Partially revert "Forbid Require inside interactive modules and module types."Gravatar Maxime Dénès2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* selective join/export of the safe_environmentGravatar Enrico Tassi2014-10-13
* Fix Declaremods.end_library (Closes: #3536)Gravatar Enrico Tassi2014-09-02
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
* STM: make -async-proofs on work from coqc tooGravatar Enrico Tassi2014-03-18
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Using hashes instead of strings in dynamic tags. In case of collision, anGravatar Pierre-Marie Pédrot2013-11-22
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Safe_typing code refactoringGravatar letouzey2013-08-20
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
* Modops.destr_functor without useless envGravatar letouzey2013-07-17
* Lib.contents () instead of Lib.contents_after NoneGravatar letouzey2013-07-17
* More dynamic argument scopesGravatar letouzey2013-07-17
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* Fix issues with "Reset Initial" in scripts given to coqtop -lGravatar letouzey2013-04-23
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Declaremods: some more minor cleanupGravatar letouzey2013-04-22
* Minor simplifications in Declaremods and Safe_typingGravatar letouzey2013-04-15
* Declaremods: drop some useless stuff (slight gain in vo size)Gravatar letouzey2013-04-15
* Modules and ppvernac, sequel of Enrico's commit 16261Gravatar letouzey2013-03-13
* Declaremods: a few syntactic improvementsGravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26