aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\
* \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\ \
| | * Univs: fix checker generating undeclared universes.Gravatar Matthieu Sozeau2015-10-02
| | * Univs: update checkerGravatar Matthieu Sozeau2015-10-02
| |/
| * Make the interface of System.raw_extern_intern much saner.Gravatar Guillaume Melquiond2015-09-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-06
|\|
| * Implementing Herbelin's fix for the "NonPar" bugGravatar mlasson2015-09-03
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * Hconsing continuedGravatar Hugo Herbelin2015-08-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|\|
| * Univs/Inductive: fix typechecking of casesGravatar Matthieu Sozeau2015-07-15
| * Updating checksum in checker (9c732a5cc continued).Gravatar Hugo Herbelin2015-07-12
| * Unused variables reported by OCaml.Gravatar Hugo Herbelin2015-07-10
| * Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| * Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Gravatar Matthieu Sozeau2015-07-09
| * Template polymorphism: A bug-fix for Bug #4258Gravatar mlasson2015-07-09
| * Checker: Report bugfixes from kernel/inductive.mlGravatar Matthieu Sozeau2015-07-08
| * Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-28
|\|
| * Adding a more efficient representation of OCaml objects in votour.Gravatar Pierre-Marie Pédrot2015-06-25
| * Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-24
|\|
| * On-demand Require.Gravatar Pierre-Marie Pédrot2015-06-24
| * Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-23
* | Merge remote-tracking branch 'forge/v8.5'Gravatar Pierre Boutillier2015-06-22
|\|
| * Votour displays wordsize of segments before loading them.Gravatar Pierre-Marie Pédrot2015-06-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-04-09
|\|
| * Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
* | Merge branch 'v8.5' into trunkGravatar Enrico Tassi2015-03-30
|\|
| * Exporting memory representation of STM tasks for votour.Gravatar Pierre-Marie Pédrot2015-03-25
| * Functorized interface over object representation in votour.Gravatar Pierre-Marie Pédrot2015-03-24
| * Fixing representation of dynamics in votour (again).Gravatar Pierre-Marie Pédrot2015-03-24
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-23
|\|
| * coqchk: more prints when -debugGravatar Enrico Tassi2015-03-23
| * Fixing internal representation of Dyn.t in votour.Gravatar Pierre-Marie Pédrot2015-03-18
| * Now accepting unit props in mutual definitionsGravatar Bruno Barras2015-03-02
* | Now accepting unit props in mutual definitionsGravatar Bruno Barras2015-03-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-26
|\|
| * Fix checker after addition of a universe context in with t := c constraints.Gravatar Matthieu Sozeau2015-02-26
* | Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-16
| * Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
| * Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
| * Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
| * Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
|/
* Fixing bug #4019, and checker blow-up at once.Gravatar Pierre-Marie Pédrot2015-02-11
* Clarifying the implementation of universe hashconsing.Gravatar Pierre-Marie Pédrot2015-02-11
* Windows: open .vo files in binary modeGravatar Enrico Tassi2015-02-05