aboutsummaryrefslogtreecommitdiff
path: root/tactics/evar_tactics.ml
AgeCommit message (Expand)Author
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-24Fixing bug #4511: evar tactic can create non-typed evars.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-29Removing the evar_map argument from s_enter.Pierre-Marie Pédrot
2015-10-20Renaming Goal.enter field into s_enter.Pierre-Marie Pédrot
2015-10-19Removing tclEVARS in various places.Pierre-Marie Pédrot
2015-10-18Making Evarutil.new_evar monotonous.Pierre-Marie Pédrot
2015-03-07Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".Hugo Herbelin
2015-01-12Update headers.Maxime Dénès
2014-11-30Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ...Hugo Herbelin
2014-11-25Used an evar name based on the local def name in "evar" tactic.Hugo Herbelin
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-09-05Adds an identifier context in pretying's Ltac context.Arnaud Spiwack
2014-08-07Better structure for Ltac pretyping environments.Pierre-Marie Pédrot
2014-08-06[uconstr]: use a closure instead of eager substitution.Arnaud Spiwack
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02More Proofview.Goal.enter.aspiwack
2013-11-02Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.aspiwack
2013-11-02Getting rid of Goal.here, and all the related exceptions and combinators.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-06-24Cleaning up the type of Tacinterp.extract_ltac_constr_values.ppedrot
2013-06-22Generalizing the use of maps instead of lists in the interpretationppedrot
2013-06-05Replacing lists by maps in matching interpretation.ppedrot
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2012-11-25Monomorphization (tactics)ppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-03-02Noise for nothingpboutill
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2010-09-17Fixed a problem introduced in r12607 after pattern_of_constr servedherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).herbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-24Fixing bug #2308 ("instantiate" tactic did not comply withherbelin
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 16:51:41 +0000