aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.mli
Commit message (Expand)AuthorAge
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Removing tactic compatibility layer in Equality.Gravatar Pierre-Marie Pédrot2014-03-26
* Moving some tactic code to the new engine.Gravatar Pierre-Marie Pédrot2014-03-26
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Clean up a warning.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Making the behavior of "injection ... as ..." more natural:Gravatar herbelin2013-06-02
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Safer, though ad hoc, approach to re-interpretation of the argument ofGravatar herbelin2009-12-28
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* adding an option functional_induction_rewrite_dependent to make functional in...Gravatar jforest2009-12-16
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06