aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.mli
Commit message (Expand)AuthorAge
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Removing the tclWEAK_PROGRESS tactical.Gravatar Pierre-Marie Pédrot2017-04-24
* Removing the tclNOTSAMEGOAL primitive from the API.Gravatar Pierre-Marie Pédrot2017-04-24
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* More self-contained code for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
* Removing unused Refiner.tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Gravatar Matthieu Sozeau2014-05-08
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Removing unused functions in Refiner.Gravatar Pierre-Marie Pédrot2014-04-06
* Removing the Change_evar refiner rule.Gravatar Pierre-Marie Pédrot2014-03-31
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* remove Refiner.abstract_tactic and similarGravatar letouzey2012-10-06
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxGravatar letouzey2012-10-06
* Added a new tactical infoH tac, that displays the names of hypothesis created...Gravatar courtieu2012-10-01
* Updating headers.Gravatar herbelin2012-08-08
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Adding the tactic "instantiate" (without argument), to force theGravatar glondu2007-12-07
* (Port of r9984) Easier debugging:Gravatar glondu2007-07-12