aboutsummaryrefslogtreecommitdiff
path: root/proofs/refiner.ml
AgeCommit message (Expand)Author
2016-08-19[pp] Fix newline issues.Emilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
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-10-21Fixed (and changed) infoH.Pierre Courtieu
2015-01-12Update headers.Maxime Dénès
2014-12-16msg_info now puts infomsg tag in emacs mode.Pierre Courtieu
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-08-18Improving error message when applying rewrite to an expression which is not a...Hugo Herbelin
2014-08-15More self-contained code for tclWITHHOLES.Pierre-Marie Pédrot
2014-08-15Removing unused Refiner.tclWITHHOLES.Pierre-Marie Pédrot
2014-06-13Improving tclWITHHOLES which did not see undefined evars up toHugo Herbelin
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-05-08- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Matthieu Sozeau
2014-05-06- Fix comparison of universes.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
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 some dead-code (thanks to ocaml warnings)Pierre Letouzey
2013-11-02Cleanup of comments.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-08-08State Transaction Machinegareuselesinge
2013-05-28Getting rid of LtacLocated exception transformer.ppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (proof)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-06remove Refiner.abstract_tactic and similarletouzey
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
2012-10-06Proof_type: rule now degenerates to prim_ruleletouzey
2012-10-06Clean-up : no more Proof_type.proof_treeletouzey
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-10-02Use the library function List.substract in prev commitletouzey
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis created...courtieu
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-30Getting rid of Pp.msgppedrot
2012-03-30info_trivial, info_auto, info_eauto, and debug (trivial|auto)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:50:43 +0000