aboutsummaryrefslogtreecommitdiff
path: root/theories/Program
AgeCommit message (Expand)Author
2016-08-19Merge remote-tracking branch 'origin/pr/246' into v8.6Matthieu Sozeau
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.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-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Experimenting removing strong normalization of the mid-statement in tactic cut.Hugo Herbelin
2015-10-07Remove the "exists" overrides from Program. (Fix bug #4360)Guillaume Melquiond
2015-06-12The "on_last_hyp" tactic now behaves as it should.Cyprien Mangin
2015-02-26Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Maxime Dénès
2015-02-23Fix some typos in comments.Guillaume Melquiond
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-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-25Forbid Require inside interactive modules and module types.Maxime Dénès
2014-09-17Add some missing Proof statements.Guillaume Melquiond
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2012-10-01Ltac repeat is in fact already doing progressletouzey
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-06-19Fix bug #2695: infinite loop in dependent destruction.msozeau
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...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-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
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
2011-06-14Making printing of backtick in Program reparsable (avoiding collision with "`(")herbelin
2011-06-07Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.msozeau
2011-04-08A module out of Program to have list notations (bug 2463)pboutill
2011-02-28Add a flag to hide obligations in Program-generated terms under anmsozeau
2011-02-17In Program obligation, do not use auto on non-proposition goals bymsozeau
2010-12-10First release of Vector library.pboutill
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-07-22Made notations for exists, exists! and notations of Utf8.v recursive notationsherbelin
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-06-08Fix unfolding tactic for well-founded Programs.msozeau
2010-05-28Correction program_simplify. Devrait corriger certaines contribs.aspiwack
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 14:46:33 +0000