aboutsummaryrefslogtreecommitdiff
path: root/theories/Program/Equality.v
AgeCommit message (Expand)Author
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-05-25Fix #12406: fix Coq type error in dependent induction's LtacPaolo G. Giarrusso
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-07-08Program: Move ProofIrrelevance to Subset.vMatthieu Sozeau
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-02-26Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Maxime Dénès
2015-02-16Fixing bug #4035 (support for dependent destruction within ltac code).Hugo Herbelin
2015-02-14dependent destruction: Fix (part of) bug #3961, by fixing dependent *Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2012-08-08Updating headers.herbelin
2012-06-19Fix bug #2695: infinite loop in dependent destruction.msozeau
2012-02-01Fix unblocking code in dependent destruction due to zeta being used in unfold...msozeau
2012-01-28Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...msozeau
2011-10-17Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...msozeau
2011-09-06Avoid registering λ and Π as keywords just for some private Local Notationletouzey
2010-10-23Used multiple lists of implicit arguments to transfer the choices ofherbelin
2010-10-03Using multiple lists of implicit arguments in Program for preservingherbelin
2010-07-31Fixed commit r13359 which was incomplete for its "trunk" part. Thanksherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-07Reorder resolution of type class and unification constraints.msozeau
2010-01-30Update CHANGES, add documentation for new commands/tactics and do a bitmsozeau
2009-11-24Minor fixes in typeclasses, avoiding repeated evar normalizations.msozeau
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-10-08Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'letouzey
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-07-20Use unfold directly in unfold_equations. Fixes test-suite.msozeau
2009-04-10Fix premature optimisation in dependent induction: even variable args needmsozeau
2009-02-04Report r11631 from 8.2 and handle non-dependent goals better inmsozeau
2008-12-14Generalized binding syntax overhaul: only two new binders: `() and `{},msozeau
2008-11-07Fix a bug in the specialization by unification tactic related to the problemsmsozeau
2008-10-19Suite 11472 et 11473herbelin
2008-09-25Various little improvements:msozeau
2008-09-15Report improvements in Equations to the dependent elimination tactic:msozeau
2008-09-13Finish debugging the unification machinery in [Equations]. Do the _compmsozeau
2008-09-12Add a type argument to letin_tac instead of using casts and recomputingmsozeau
2008-09-11Add enough information to correctly globalize recursive calls in inductive andmsozeau
2008-09-09Fix a bug reintroduced in [setoid_reflexivity] etc...msozeau
2008-09-07More debugging of [Equations], now able to discharge even the heavilymsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:19:11 +0000