aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
AgeCommit message (Expand)Author
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-02-28[toplevel] Update state when `Drop` exception is thrown [#6872]Emilio Jesus Gallego Arias
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-19Merge PR #6753: [toplevel] Make toplevel state into a record.Maxime Dénès
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2018-02-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
2018-01-18Merge PR #6448: Cleanup and add debug printers a bitMaxime Dénès
2017-12-27[API] remove large file containing duplicate interfacesEnrico Tassi
2017-12-22Cleanup debug printers a bit, add generated mli.Gaëtan Gilbert
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
2017-11-21Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Maxime Dénès
2017-11-19[parser] Remove unnecessary statically initialized hook.Emilio Jesus Gallego Arias
2017-11-15[dev] Remove deprecation warning from `base_include`Emilio Jesus Gallego Arias
2017-10-28[toplevel] Export the last document seen after `Drop`.Emilio Jesus Gallego Arias
2017-07-27[api] Fix base_include LTAC parts.Emilio Jesus Gallego Arias
2017-07-16Adapting to 91df40272 (body_of_constant_body moved to global).Hugo Herbelin
2017-06-16Fix a bug in cumulativityAmin Timany
2017-06-16A short cleanupAmin Timany
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-15fix dev/base_include (thanks Zimmi48)Pierre Letouzey
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-04-07Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)Matthieu Sozeau
2017-02-23Fixing #use"include" after vernac is added and ltac is moved to a plugin.Hugo Herbelin
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-07-03rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Pierre Letouzey
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Fixing another instance of bug #3267 in eauto, this time in theHugo Herbelin
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-21Fixing #4198 (looking for subterms also in the return clause of match).Hugo Herbelin
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
2014-12-07Removing import of Proofview in debugger because its module Goal hidesHugo Herbelin
2014-10-31More "open" by default for trace debugging.Hugo Herbelin
2014-10-15Fix ill-typed debugging functionMatthieu Sozeau
2014-10-10Add debug printers for projections, fix printing of evar constraintsMatthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-12Fix base_include due to change in argument order of env and evar_mapMatthieu Sozeau
2014-06-28More open in base_includeHugo Herbelin
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-06Remove Lemmas from base_include, it's not linked in dev/printers anymoreMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-01Updated debugging printersHugo Herbelin
2014-02-24app_node, stack, state printersPierre Boutillier
2014-01-11'Pretty' printer for wf_pathsPierre
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:03:25 +0000