aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extraargs.ml4
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
* Retroknowledge arguments are made VERNAC ARGUMENTS.Gravatar Pierre-Marie Pédrot2014-09-13
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Ensuring the right parsing of glob arguments, used by refineGravatar Pierre-Marie Pédrot2013-12-01
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
* Tacinterp: fewer use of old-style goals.Gravatar Arnaud Spiwack2013-11-25
* Now, idtac closures use maps instead of association list.Gravatar ppedrot2013-06-22
* Moving coercion functions out of Tacinterp.Gravatar ppedrot2013-06-12
* Hiding tactic value representations.Gravatar ppedrot2013-06-10
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Modulification of identifierGravatar ppedrot2012-12-14
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Fixing Show Script issues.Gravatar ppedrot2012-09-20
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Corrects a (very) longstanding bug of tactics. As is were, tactic expectingGravatar aspiwack2012-04-18
* Removing redundant entry int_nelist and removing extra space whenGravatar herbelin2012-03-18
* 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
* ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDGravatar glondu2010-12-25
* 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
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fixed some printing bugs.Gravatar herbelin2010-04-18
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* 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
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* 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
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* killing some more non-exhaustive patternsGravatar letouzey2007-06-26
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-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
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* Diverses corrections de l'afficheur et du traducteur pour s'assurer deGravatar herbelin2006-04-26
* Standardisation du nom de subst_raw en subst_rawconstrGravatar herbelin2006-01-11