aboutsummaryrefslogtreecommitdiff
path: root/tactics/tauto.ml4
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-06-27Removing useless tactic arguments, and using generic argumentsppedrot
2013-06-22Now, idtac closures use maps instead of association list.ppedrot
2013-06-10Hiding tactic value representations.ppedrot
2013-02-19Dir_path --> DirPathletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (tactics)ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-08Updating headers.herbelin
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-15Intuition: temporary(?) restore the unconditional unfolding of notletouzey
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-04-12"A -> B" is a notation for "forall _ : A, B".pboutill
2012-03-02Noise for nothingpboutill
2012-01-31Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...msozeau
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be t...msozeau
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-10-25Applying Tom Prince's patch to support parametric "constructor n" inherbelin
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-04Changed the way to support compatibility with previous versions.herbelin
2009-09-26Fixed a hole in glob_tactic that allowed some Ltac code to refer toherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-04-10Fix tauto no longer failing after commit 12077; appropriate errorherbelin
2009-04-09Turning tauto into a classical tautology prover as soon as classicalherbelin
2009-01-29Solves some warning and hides some not-bad ones in doc. It remains aherbelin
2008-12-30- Fixed bugs and compatibilities issues in herbelin
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-07-25More compatibility fixes, revert the tauto fix that preventedmsozeau
2008-07-24Tauto breaking not only binary "conjunctions" seems like a bad ideamsozeau
2008-07-22A try at allowing matching on applications as a binary syntax node by default.msozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-03-30Modifications diverses et variées :herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2004-07-16Nouvelle en-têteherbelin
2003-12-23*** empty log message ***barras
2003-11-12petits changements de syntaxebarras
2003-10-16nouvelle syntaxe de ltacbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 23:41:09 +0000