aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/autorewrite.ml
Commit message (Expand)AuthorAge
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * Merge branch 'master' into ltac2-hooksGravatar Pierre-Marie Pédrot2017-05-19
| | |\ | | |/ | |/|
| * | Remove two unused opens.Gravatar Maxime Dénès2017-05-05
| | * Allowing to pass arbitrary data in internalization environments.Gravatar Pierre-Marie Pédrot2017-05-03
| * | Removing dead code in Autorewrite.Gravatar Pierre-Marie Pédrot2017-05-01
| |/
* / [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Unplugging Pptactic from Ppvernac.Gravatar Pierre-Marie Pédrot2016-09-08
* 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
* Unify location handling of error functions.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
* Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Getting rid of the Geninterp.generic_interp function.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving Autorewrite back to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
* 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
* | Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.Gravatar Pierre-Marie Pédrot2016-01-09
* | Removing the evar_map argument from s_enter.Gravatar Pierre-Marie Pédrot2015-10-29
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
* | Renaming Goal.enter field into s_enter.Gravatar Pierre-Marie Pédrot2015-10-20
* | Removing tclEVARS in various places.Gravatar Pierre-Marie Pédrot2015-10-19
|/
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* refresh metas in rewrite hints loaded from .vo files (fix bug #3815)Gravatar Nickolai Zeldovich2015-04-06
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing bug #3796.Gravatar Pierre-Marie Pédrot2014-12-17
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05