aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.ml
Commit message (Expand)AuthorAge
* infoH: output via msg_* to make the XML protocol happyGravatar Enrico Tassi2016-08-17
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fixed (and changed) infoH.Gravatar Pierre Courtieu2015-10-21
* Update headers.Gravatar Maxime Dénès2015-01-12
* msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Improving error message when applying rewrite to an expression which is not a...Gravatar Hugo Herbelin2014-08-18
* More self-contained code for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
* Removing unused Refiner.tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
* Improving tclWITHHOLES which did not see undefined evars up toGravatar Hugo Herbelin2014-06-13
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Gravatar Matthieu Sozeau2014-05-08
* - Fix comparison of universes.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* 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 some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Cleanup of comments.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Getting rid of LtacLocated exception transformer.Gravatar ppedrot2013-05-28
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* Removing Exc_located and using the new exception enrichementGravatar ppedrot2013-02-18
* Revised the Ltac trace mechanism so that trace breaking due toGravatar herbelin2013-02-17
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (proof)Gravatar ppedrot2012-11-25
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* remove Refiner.abstract_tactic and similarGravatar letouzey2012-10-06
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* Proof_type: rule now degenerates to prim_ruleGravatar letouzey2012-10-06
* Clean-up : no more Proof_type.proof_treeGravatar letouzey2012-10-06
* Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxGravatar letouzey2012-10-06
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Use the library function List.substract in prev commitGravatar letouzey2012-10-02
* Added a new tactical infoH tac, that displays the names of hypothesis created...Gravatar courtieu2012-10-01
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
* Noise for nothingGravatar pboutill2012-03-02
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fix commentGravatar glondu2010-06-07