index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
dev
/
base_include
Age
Commit message (
Expand
)
Author
2020-08-27
[numeral] [plugins] Switch from `Big_int` to ZArith.
Emilio Jesus Gallego Arias
2020-06-29
Refining out the Refiner.
Pierre-Marie Pédrot
2020-06-26
[declare] [api] Removal of deprecated functions
Emilio Jesus Gallego Arias
2020-06-24
Merge Clenvtac into Clenv.
Pierre-Marie Pédrot
2020-04-21
[declare] [tactics] Move declare to `vernac`
Emilio Jesus Gallego Arias
2019-12-22
Rename files with Class in their name to make their role clearer.
Pierre-Marie Pédrot
2019-07-07
[error] Remove special error printing pre-processing
Emilio Jesus Gallego Arias
2019-06-24
[test-suite] Fix printers test
Gaëtan Gilbert
2019-05-28
Fix [Drop. #use "include";;] for indirect_accessor
Gaë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-18
Remove reference name type.
Maxime Dénès
2018-06-12
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-05-30
Merge 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-25
Remove some occurrences of Evd.empty
Maxime 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-04
Merge 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-19
Merge PR #6753: [toplevel] Make toplevel state into a record.
Maxime Dénès
2018-02-17
Change references to CAMLP4 to CAMLP5 to be more accurate since we no
Jim Fehrle
2018-02-15
[toplevel] Make toplevel state into a record.
Emilio Jesus Gallego Arias
2018-01-18
Merge PR #6448: Cleanup and add debug printers a bit
Maxime Dénès
2017-12-27
[API] remove large file containing duplicate interfaces
Enrico Tassi
2017-12-22
Cleanup debug printers a bit, add generated mli.
Gaëtan Gilbert
2017-12-20
Separate 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-21
Merge 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-16
Adapting to 91df40272 (body_of_constant_body moved to global).
Hugo Herbelin
2017-06-16
Fix a bug in cumulativity
Amin Timany
2017-06-16
A short cleanup
Amin Timany
2017-06-16
Clean up universes of constants and inductives
Amin Timany
2017-06-15
fix dev/base_include (thanks Zimmi48)
Pierre Letouzey
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-04-07
Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)
Matthieu Sozeau
2017-02-23
Fixing #use"include" after vernac is added and ltac is moved to a plugin.
Hugo Herbelin
2016-09-14
Moving Ltac-specific parsing API to ltac/ folder.
Pierre-Marie Pédrot
2016-07-03
rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...
Pierre Letouzey
2016-03-21
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
[next]