aboutsummaryrefslogtreecommitdiff
path: root/proofs/refiner.mli
AgeCommit message (Expand)Author
2020-06-29Refining out the Refiner.Pierre-Marie Pédrot
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-29Moving the remaining Refiner functions to Tacmach.Pierre-Marie Pédrot
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-06-29Remove the deprecated functions from refiner, moving them to Tacticals.Pierre-Marie Pédrot
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-03Remove a very specific low-level tactical from Refiner.Pierre-Marie Pédrot
2020-05-03Wrap Refiner.refiner in the tactic monad.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update 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-14Deprecate Refiner [evar_map ref] exported functions.Gaëtan Gilbert
2018-02-27Update 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-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-24Removing the tclWEAK_PROGRESS tactical.Pierre-Marie Pédrot
2017-04-24Removing the tclNOTSAMEGOAL primitive from the API.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-01-12Update headers.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-08-15More self-contained code for tclWITHHOLES.Pierre-Marie Pédrot
2014-08-15Removing unused Refiner.tclWITHHOLES.Pierre-Marie Pédrot
2014-06-10Cleanup 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-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-06Removing unused functions in Refiner.Pierre-Marie Pédrot
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-08-08State Transaction Machinegareuselesinge
2013-04-29Merging Context and Sign.ppedrot
2012-10-06remove Refiner.abstract_tactic and similarletouzey
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis created...courtieu
2012-08-08Updating headers.herbelin
2012-03-30info_trivial, info_auto, info_eauto, and debug (trivial|auto)letouzey
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:08:17 +0000