aboutsummaryrefslogtreecommitdiff
path: root/theories/Program
AgeCommit message (Expand)Author
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
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-09-06Bound proof-search in default program obligation tactic.Matthieu Sozeau
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-09Remove most uses of function extensionality in Program.CombinatorsJasper Hugunin
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:24:48 +0000