aboutsummaryrefslogtreecommitdiff
path: root/tactics/extraargs.mli
AgeCommit message (Expand)Author
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-02-22The tactic generic argument now returns a value rather than a glob_expr.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-09-13Retroknowledge arguments are made VERNAC ARGUMENTS.Pierre-Marie Pédrot
2014-04-14Closing bug #3260Julien Forest
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-12-01Ensuring the right parsing of glob arguments, used by refinePierre-Marie Pédrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-02Noise for nothingpboutill
2010-12-27Rename the "raw" argument extension into "glob"glondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-08-03Export printing functions for extra arguments. Maybe there's a way tomsozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-04-24Fixing bug #2308 ("instantiate" tactic did not comply withherbelin
2009-01-18Getting rid of the previous implementation of setoid_rewrite which wasmsozeau
2008-10-26Fixes and refinements regarding occurrence selection:herbelin
2008-04-20Work on the "occurrences" tactic argument. It is now possible to passmsozeau
2008-04-12Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.msozeau
2008-01-30Add occurence extra argmsozeau
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2006-08-23Bug in replace tactics introduced in r9073 (overlap between replace .. with a...jforest
2006-08-22Forgot a file in previous commit jforest
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-09-29Hugly temporary notationsacerdot
2004-09-24New: (temporary) concrete syntax to specify the morphism signature:sacerdot
2004-07-16Nouvelle en-têteherbelin
2004-06-29moved instantiate binding to extratacticscorbinea
2003-11-08Code obsoleteherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:43:31 +0000