aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2017-03-03Merge PR#273: Tidy stdlibMaxime Dénès
2017-03-03Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.Hugo Herbelin
2017-03-03Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.Hugo Herbelin
2017-03-03Completing "few lemmas about Zneg" with lemmas also about Zpos.Hugo Herbelin
2017-03-03A couple of other useful properties about compare_cont.Hugo Herbelin
2017-03-03Compatibility of iff wrt not and imp.Hugo Herbelin
2017-03-03Formatting references with surrounding brackets in Diaconescu.v.Hugo Herbelin
2017-03-01Add η principles for sigma typesJason Gross
2017-03-01Remove some trailing whitespace in Init/Specif.vJason Gross
2017-02-24Simplifying the proof of NoRetractToModalProposition.paradox inHugo Herbelin
2017-02-23Fixing a little bug in printing ex2 (type was printed "_" by default).Hugo Herbelin
2017-02-21Allow interactive editing of Coq.Init.LogicJason Gross
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2017-02-15Added some theory on powerRZ.Thomas Sibut-Pinote
2017-01-30Proof clean-up.Théo Zimmermann
2016-12-26Fix some documentation typos.Guillaume Melquiond
2016-12-19Fix a typo in Hurkens.v commentJason Gross
2016-12-11strengthened the statement of JMeq_eq_depAbhishek Anand
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
2016-11-04Silence option deprecation warnings in the compat fileJason Gross
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-10-22Add Unset Use Unif Heuristics in Compat/Coq85Matthieu Sozeau
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-17Fix previous commit.Pierre-Marie Pédrot
2016-10-17Merge PR #300 into v8.6Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-12Little addition to 6eede071 for consistency of style in OrdersFacts.v.Hugo Herbelin
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-06Fixing unexpected "noise" introduced in commit 24d5448c.Hugo Herbelin
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-05Clean up type classes flags and update compat file.Maxime Dénès
2016-10-03Remove if_then_else. Use tryif instead.Théo Zimmermann
2016-10-02More tests for tactic "subst".Hugo Herbelin
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-29Move vector/list compat notations to their relevant filesJason Gross
2016-09-28ZDivEucl: notations in different scope to avoid a warningPierre Letouzey
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-26Remove spaces from around list notationsJason Gross
2016-09-26Remove spaces from around vector notationsJason Gross
2016-09-26Unbreak Ltac [ | .. | ] notation in -compat 8.5Jason Gross
2016-09-26Fix bug #4785 (use [ ] for vector nil)Jason Gross
2016-09-23Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-19extensionality: Handle dependently-used hypothesesJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 20:47:30 +0000