aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
AgeCommit message (Expand)Author
2021-01-27[sysinit] new component for system initializationEnrico Tassi
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
2020-06-29Refining out the Refiner.Pierre-Marie Pédrot
2020-06-26[declare] [api] Removal of deprecated functionsEmilio Jesus Gallego Arias
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-06-24[test-suite] Fix printers testGaëtan Gilbert
2019-05-28Fix [Drop. #use "include";;] for indirect_accessorGaëtan Gilbert
2019-02-18[dev] Add include versions for Dune builds.Emilio Jesus Gallego Arias
2018-11-21[camlp5] Remove dependency on camlp5.Emilio Jesus Gallego Arias
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-30Merge PR #7558: [api] Make `vernac/` self-contained.Maxime Dénès
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
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