aboutsummaryrefslogtreecommitdiff
path: root/tactics/evar_tactics.mli
AgeCommit message (Expand)Author
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
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-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-24Fixing bug #2308 ("instantiate" tactic did not comply withherbelin
2008-10-26Fixes and refinements regarding occurrence selection:herbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-07-16Nouvelle en-têteherbelin
2004-06-28more evar stuffcorbinea
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:53:48 +0000