aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.mli
AgeCommit message (Expand)Author
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-03-05Exporting build_selector, a component of discriminate, for use in congruence.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-10-13Fix some typos.Guillaume Melquiond
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-08-18Lazy interpretation of patterns so that expressions such as "intros H H'/H"Hugo Herbelin
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-03-26Removing tactic compatibility layer in Equality.Pierre-Marie Pédrot
2014-03-26Moving some tactic code to the new engine.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02Clean up a warning.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-06-02Making the behavior of "injection ... as ..." more natural:herbelin
2013-05-12Use the Hook module here and there.ppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces: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-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Noise for nothingpboutill
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-12-28Safer, though ad hoc, approach to re-interpretation of the argument ofherbelin
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-16adding an option functional_induction_rewrite_dependent to make functional in...jforest
2009-12-12Updated compatibility for rewriting equality proofs that are dependentherbelin
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-08Fix the bug-ridden code used to choose leibniz or generalizedmsozeau
2009-08-06Move out JMeq of subst for compatibility (it affects e.g. theherbelin
2009-07-24Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"letouzey
2009-06-30Add new variants of [rewrite] and [autorewrite] which differ in themsozeau
2009-04-08Some dead code removal + cleanupsletouzey
2008-11-05Port [rewrite] tactics to open terms. Currently no check that evarsmsozeau
2008-08-04Évolutions diverses et variées.herbelin
2008-07-26Even better test for choosing rewrite or setoid_rewrite.msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 05:44:27 +0000