aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eqdecide.ml4
Commit message (Expand)AuthorAge
* remove Refiner.abstract_tactic and similarGravatar letouzey2012-10-06
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* 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
* Noise for nothingGravatar pboutill2012-03-02
* tactics/eqdecide.ml4: avoid a useless argument in decideEqualityGravatar glondu2010-12-24
* Remove the two-argument variant of "decide equality"Gravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
* - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deGravatar herbelin2006-03-22
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Types inductifs parametriquesGravatar mohring2005-11-02
* Nouvelle en-têteGravatar herbelin2004-07-16
* Restructuration des procédures de filtrageGravatar herbelin2003-05-19
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...Gravatar herbelin2002-06-05
* Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...Gravatar herbelin2002-06-05
* Fichiers tactics/*.ml4 remplacent les tactics/*.vGravatar herbelin2002-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-12 07:04:15 +0000