aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program/Equality.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Program: Move ProofIrrelevance to Subset.vGravatar Matthieu Sozeau2016-07-08
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Gravatar Maxime Dénès2015-02-26
* Fixing bug #4035 (support for dependent destruction within ltac code).Gravatar Hugo Herbelin2015-02-16
* dependent destruction: Fix (part of) bug #3961, by fixing dependent *Gravatar Matthieu Sozeau2015-02-14
* Update headers.Gravatar Maxime Dénès2015-01-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Updating headers.Gravatar herbelin2012-08-08
* Fix bug #2695: infinite loop in dependent destruction.Gravatar msozeau2012-06-19
* Fix unblocking code in dependent destruction due to zeta being used in unfold...Gravatar msozeau2012-02-01
* Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...Gravatar msozeau2012-01-28
* Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...Gravatar msozeau2011-10-17
* Avoid registering λ and Π as keywords just for some private Local NotationGravatar letouzey2011-09-06
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
* Using multiple lists of implicit arguments in Program for preservingGravatar herbelin2010-10-03
* Fixed commit r13359 which was incomplete for its "trunk" part. ThanksGravatar herbelin2010-07-31
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Use unfold directly in unfold_equations. Fixes test-suite.Gravatar msozeau2009-07-20
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* Fix a bug in the specialization by unification tactic related to the problemsGravatar msozeau2008-11-07
* Suite 11472 et 11473Gravatar herbelin2008-10-19
* Various little improvements:Gravatar msozeau2008-09-25
* Report improvements in Equations to the dependent elimination tactic:Gravatar msozeau2008-09-15
* Finish debugging the unification machinery in [Equations]. Do the _compGravatar msozeau2008-09-13
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Fix a bug reintroduced in [setoid_reflexivity] etc...Gravatar msozeau2008-09-09
* More debugging of [Equations], now able to discharge even the heavilyGravatar msozeau2008-09-07
* Better handling of recursive Equations definitions... still not perfect.Gravatar msozeau2008-09-03
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
* Add support for recursive definitions to [Equations], deciding if aGravatar msozeau2008-09-02
* Initial implementation of a new command to define (dependent) functions byGravatar msozeau2008-09-02
* Fixes in dependent induction tactic to keep names, allow givingGravatar msozeau2008-08-21
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
* Add test-suite file for bug# 1905 and minor fix in Program/Equality.Gravatar msozeau2008-07-22
* Improve the dependent induction tactic to automatically find theGravatar msozeau2008-05-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 10:37:53 +0000