aboutsummaryrefslogtreecommitdiff
path: root/theories/Vectors/VectorDef.v
AgeCommit message (Expand)Author
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-10-11Modify Vectors/VectorDef.v to compile with -mangle-namesJasper Hugunin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-09-01edits per reviewYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
2019-06-20Fix coqdoc title: should be on a single line.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
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-17Strings: add ByteVectorYishuai Li
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-07-30Vector: expose ++ to userYishuai Li
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-03-30Added take to VectorDef.George Stelle
2016-09-29Move vector/list compat notations to their relevant filesJason Gross
2016-09-26Remove spaces from around vector notationsJason Gross
2016-09-26Fix bug #4785 (use [ ] for vector nil)Jason Gross
2016-04-25Fixing bug #4684: Singleton list notation unusable in 8.5pl1.Pierre-Marie Pédrot
2014-07-22Simplified rect2, it turns out Arthur's trick was not required.Maxime Dénès
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
2013-03-25Normalized type for Vector.map2pboutill
2013-02-25cbn friendly VectorDefpboutill
2013-01-18Unset Asymmetric Patternspboutill
2012-05-25Bugs revealed by playing with contribspboutill
2012-05-11Vectors takes advantage of pattern matching compiler fixuppboutill
2012-02-29Vector: missing injection lemmas and better impossible branchespboutill
2011-12-07Vectors use a bit more the pattern matching compilerpboutill
2011-11-21VectorDef.v takes benefit of dependencies being taken into accountherbelin
2011-08-10Less ambitious application of a notation for eq_rect. We proposedherbelin
2011-08-08New proposition "rewrite Heq in H" for eq_rect (assuming that there isherbelin
2011-07-16Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)herbelin
2011-05-03As many notation for for vectors as for List.pboutill
2011-03-23- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...msozeau
2011-03-11Inference of match predicate produces ill-typed unification problem,msozeau
2011-02-10Vectors fully use implicit argumentspboutill
2011-02-10Fixpoints are traverse during implicits arguments search to toplevelpboutill
2011-02-10Interp a definition with the implicit arguments of its local contextpboutill
2011-02-10local variables can have implicits locallypboutill
2011-02-10Data structure telling implicits of local variables is a map in thepboutill
2010-12-10First release of Vector library.pboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:50:37 +0000