aboutsummaryrefslogtreecommitdiff
path: root/tactics/eqdecide.ml
AgeCommit message (Expand)Author
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-01Removing some tactic compatibility layer.Pierre-Marie Pédrot
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-27Removing tactic compatibility layer from Eqdecide.Pierre-Marie Pédrot
2014-03-26Adding an interface to Eqdecide and putting the grammar rules in a dedicatedPierre-Marie Pédrot
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
2002-02-15petits changements cosmetiques sur les tactiquesbarras
2001-11-05GROS COMMIT:barras
2001-03-15entetesfilliatr
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...herbelin
2001-02-06EqDecidefilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:16:23 +0000