aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tauto.ml4
Commit message (Expand)AuthorAge
* Removing antiquotations in Tauto.Gravatar Pierre-Marie Pédrot2014-09-08
* Proper interpretation function for tauto.Gravatar Pierre-Marie Pédrot2014-09-06
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* 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
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Removing useless tactic arguments, and using generic argumentsGravatar ppedrot2013-06-27
* Now, idtac closures use maps instead of association list.Gravatar ppedrot2013-06-22
* Hiding tactic value representations.Gravatar ppedrot2013-06-10
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (tactics)Gravatar ppedrot2012-11-25
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Intuition: temporary(?) restore the unconditional unfolding of notGravatar letouzey2012-05-15
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* "A -> B" is a notation for "forall _ : A, B".Gravatar pboutill2012-04-12
* Noise for nothingGravatar pboutill2012-03-02
* Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...Gravatar msozeau2012-01-31
* Tentative to fix bug #2628 by not letting intuition break records. Might be t...Gravatar msozeau2012-01-28
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* Applying Tom Prince's patch to support parametric "constructor n" inGravatar herbelin2011-10-25
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
* Fixed a hole in glob_tactic that allowed some Ltac code to refer toGravatar herbelin2009-09-26
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Fix tauto no longer failing after commit 12077; appropriate errorGravatar herbelin2009-04-10
* Turning tauto into a classical tautology prover as soon as classicalGravatar herbelin2009-04-09
* Solves some warning and hides some not-bad ones in doc. It remains aGravatar herbelin2009-01-29
* - Fixed bugs and compatibilities issues in Gravatar herbelin2008-12-30
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* More compatibility fixes, revert the tauto fix that preventedGravatar msozeau2008-07-25
* Tauto breaking not only binary "conjunctions" seems like a bad ideaGravatar msozeau2008-07-24
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22