aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extraargs.mli
Commit message (Expand)AuthorAge
* Retroknowledge arguments are made VERNAC ARGUMENTS.Gravatar Pierre-Marie Pédrot2014-09-13
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Ensuring the right parsing of glob arguments, used by refineGravatar Pierre-Marie Pédrot2013-12-01
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
* Noise for nothingGravatar pboutill2012-03-02
* Rename the "raw" argument extension into "glob"Gravatar glondu2010-12-27
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Export printing functions for extra arguments. Maybe there's a way toGravatar msozeau2010-08-03
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Add occurence extra argGravatar msozeau2008-01-30
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Bug in replace tactics introduced in r9073 (overlap between replace .. with a...Gravatar jforest2006-08-23
* Forgot a file in previous commit Gravatar jforest2006-08-22
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Hugly temporary notationGravatar sacerdot2004-09-29
* New: (temporary) concrete syntax to specify the morphism signature:Gravatar sacerdot2004-09-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* Code obsoleteGravatar herbelin2003-11-08
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29