| Age | Commit message (Expand) | Author |
|---|
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann |
| 2019-05-29 | [proofs] Remove unused API [detected by coverage] | Emilio Jesus Gallego Arias |
| 2018-11-21 | [legacy proof engine] Remove some cruft. | Emilio Jesus Gallego Arias |
| 2018-10-06 | [api] Remove (most) 8.9 deprecated objects. | Emilio Jesus Gallego Arias |
| 2018-05-14 | Deprecate Refiner [evar_map ref] exported functions. | Gaëtan Gilbert |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2017-12-09 | [api] Remove yet another type alias. | Emilio Jesus Gallego Arias |
| 2017-11-13 | [api] Insert miscellaneous API deprecation back to core. | Emilio Jesus Gallego Arias |
| 2017-11-06 | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-04-24 | Removing the tclWEAK_PROGRESS tactical. | Pierre-Marie Pédrot |
| 2017-04-24 | Removing the tclNOTSAMEGOAL primitive from the API. | Pierre-Marie Pédrot |
| 2017-02-14 | Definining EConstr-based contexts. | Pierre-Marie Pédrot |
| 2016-06-09 | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot |
| 2014-08-15 | More self-contained code for tclWITHHOLES. | Pierre-Marie Pédrot |
| 2014-08-15 | Removing unused Refiner.tclWITHHOLES. | Pierre-Marie Pédrot |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-05-08 | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ... | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2014-04-06 | Removing unused functions in Refiner. | Pierre-Marie Pédrot |
| 2014-03-31 | Removing the Change_evar refiner rule. | Pierre-Marie Pédrot |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2012-10-06 | remove Refiner.abstract_tactic and similar | letouzey |
| 2012-10-06 | Clean-up : removal of Proof_type.tactic_expr | letouzey |
| 2012-10-06 | Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box | letouzey |
| 2012-10-01 | Added a new tactical infoH tac, that displays the names of hypothesis created... | courtieu |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-30 | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey |
| 2011-03-18 | A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-06-11 | Use a lazy value for the message in FailError, so that it won't be | msozeau |
| 2009-05-20 | - Fixing declarative mode in presence of high use of Change_evars nodes | herbelin |
| 2009-03-14 | Cleaning/uniformizing the interface of tacticals.mli | herbelin |
