aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eqdecide.ml
Commit message (Expand)AuthorAge
* Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Replacing tclENV with the goal environmentGravatar amblaf2017-07-31
* Remove references to Global.env in tactics/*.mlGravatar amblaf2017-07-31
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* tactics cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
* [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Remove unused open.Gravatar Maxime Dénès2017-05-05
* Merge PR#541: Fixing "decide equality" bug #5449Gravatar Maxime Dénès2017-05-03
|\
| * Fixing "decide equality"'s bug #5449.Gravatar Hugo Herbelin2017-04-30
* | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
|/
* 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
* Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Eqdecide API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* 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
* Moving Eqdecide to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
* Removing useless grammar.cma dependencies.Gravatar Pierre-Marie Pédrot2016-03-06
* Moving conversion functions to the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
|/
* Fix for bug #4280: "decide equality produces terms that don't compute well".Gravatar Pierre-Marie Pédrot2015-07-28
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing tactic compatibility layer from Eqdecide.Gravatar Pierre-Marie Pédrot2014-03-27
* Adding an interface to Eqdecide and putting the grammar rules in a dedicatedGravatar Pierre-Marie Pédrot2014-03-26
* Fichiers tactics/*.ml4 remplacent les tactics/*.vGravatar herbelin2002-05-29
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* GROS COMMIT:Gravatar barras2001-11-05
* entetesGravatar filliatr2001-03-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-16 00:17:36 +0000