aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/base_include
Commit message (Expand)AuthorAge
* [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\
* | [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Emilio Jesus Gallego Arias2018-02-28
| * [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
|/
* Merge PR #6753: [toplevel] Make toplevel state into a record.Gravatar Maxime Dénès2018-02-19
|\
* | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| * [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
|/
* Merge PR #6448: Cleanup and add debug printers a bitGravatar Maxime Dénès2018-01-18
|\
* | [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| * Cleanup debug printers a bit, add generated mli.Gravatar Gaëtan Gilbert2017-12-22
* | Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* | [vernac] Split `command.ml` into separate files.Gravatar Emilio Jesus Gallego Arias2017-12-17
|/
* Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Gravatar Maxime Dénès2017-11-21
|\
| * [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
* | [dev] Remove deprecation warning from `base_include`Gravatar Emilio Jesus Gallego Arias2017-11-15
|/
* [toplevel] Export the last document seen after `Drop`.Gravatar Emilio Jesus Gallego Arias2017-10-28
* [api] Fix base_include LTAC parts.Gravatar Emilio Jesus Gallego Arias2017-07-27
* Adapting to 91df40272 (body_of_constant_body moved to global).Gravatar Hugo Herbelin2017-07-16
* Fix a bug in cumulativityGravatar Amin Timany2017-06-16
* A short cleanupGravatar Amin Timany2017-06-16
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* fix dev/base_include (thanks Zimmi48)Gravatar Pierre Letouzey2017-06-15
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)Gravatar Matthieu Sozeau2017-04-07
* Fixing #use"include" after vernac is added and ltac is moved to a plugin.Gravatar Hugo Herbelin2017-02-23
* Moving Ltac-specific parsing API to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-14
* rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
|\
| * Fixing another instance of bug #3267 in eauto, this time in theGravatar Hugo Herbelin2015-10-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Fixing #4198 (looking for subterms also in the return clause of match).Gravatar Hugo Herbelin2015-04-21
* | Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27
|/
* Removing import of Proofview in debugger because its module Goal hidesGravatar Hugo Herbelin2014-12-07
* More "open" by default for trace debugging.Gravatar Hugo Herbelin2014-10-31
* Fix ill-typed debugging functionGravatar Matthieu Sozeau2014-10-15
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Fix base_include due to change in argument order of env and evar_mapGravatar Matthieu Sozeau2014-09-12
* More open in base_includeGravatar Hugo Herbelin2014-06-28
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Remove Lemmas from base_include, it's not linked in dev/printers anymoreGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Updated debugging printersGravatar Hugo Herbelin2014-04-01
* app_node, stack, state printersGravatar Pierre Boutillier2014-02-24
* 'Pretty' printer for wf_pathsGravatar Pierre2014-01-11
* Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evdGravatar Pierre Letouzey2014-01-08
* Remove the Hiddentac module.Gravatar Arnaud Spiwack2013-11-25
* Removes Refine from the dev tools now that the module has been deleted.Gravatar aspiwack2013-11-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-22 11:00:53 +0000