aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eqdecide.ml
Commit message (Expand)AuthorAge
* 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
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* EqDecideGravatar filliatr2001-02-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 01:17:04 +0000