aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Specif.v
AgeCommit message (Expand)Author
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-08-20Modify Init/Specif.v to compile with -mangle-namesJasper Hugunin
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2020-03-30new sig notations and spaces addedOlivier Laurent
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-19Choosing a standard format for the "rew dependent" notation.Hugo Herbelin
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-02Remove -compat 8.7Jason Gross
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-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-02Update compat notations to be compat 8.7Jason Gross
2018-09-25Adding lemmas about dependent equality.Hugo Herbelin
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-03-08Merge PR #6743: Add notation {x & P} for sigTMaxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-20Trying a hack to support {'pat|P} without breaking compatibility.Hugo Herbelin
2018-02-20Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Hugo Herbelin
2018-02-12Add notation {x & P} for sigTTej Chajed
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-28More uniform indentation of sigma lemmasJason Gross
2017-05-28Give explicit proof terms to proj2_sig_eq etc.Jason Gross
2017-05-28Add some more comments about sigma equalitiesJason Gross
2017-05-28Remove motive argument from [rew dependent]Jason Gross
2017-05-28Use a local [rew dependent] notationJason Gross
2017-05-28Add forward-chaining versions: [eq_sig*_uncurried]Jason Gross
2017-05-28Use notation for sigTJason Gross
2017-05-28Remove reference to [IsIso]Jason Gross
2017-05-28Use notations for [sig], [sigT], [sig2], [sigT2]Jason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
2017-05-28Add equality lemmas for sig2 and sigT2Jason Gross
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
2017-05-28Add lemmas about equality of sigma typesJason Gross
2017-04-30Functional choice <-> [inhabited] and [forall] commuteGaetan Gilbert
2017-03-01Add η principles for sigma typesJason Gross
2017-03-01Remove some trailing whitespace in Init/Specif.vJason Gross
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-06-16Adding option "Set Reversible Pattern Implicit" to Specif.v so that anHugo Herbelin
2016-04-27Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Hugo Herbelin
2016-04-27Adding option "Set Reversible Pattern Implicit" to Specif.v so that anHugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Adding a notation { x & P } for { x : _ & P }.Hugo Herbelin
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:39:47 +0000