aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.ml
Commit message (Expand)AuthorAge
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* 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
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* \ Merge remote-tracking branch 'v8.6' into trunkGravatar Matej Kosik2016-08-25
|\ \
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| | * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| |/ |/|
| * [pp] Fix newline issues.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-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
|/
* 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