aboutsummaryrefslogtreecommitdiff
path: root/theories/Program
AgeCommit message (Expand)Author
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-11-13Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freeLi-yao Xia
2020-05-25Fix #12406: fix Coq type error in dependent induction's LtacPaolo G. Giarrusso
2020-04-30do not re-export ListNotations from ProgramAntonio Nikishaev
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
2019-11-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
2019-11-26Make rapply handle all numbers of underscoresJason Gross
2019-11-26Remove some trailing whitespace in theories/Program/Tactics.vJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:49:42 +0000