aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2017-03-03Logic library: Adding a characterization of excluded-middle in term ofHugo Herbelin
2017-03-03Formatting references with surrounding brackets in Diaconescu.v.Hugo Herbelin
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2016-12-19Fix a typo in Hurkens.v commentJason Gross
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
2016-09-19Adding an "extensionality in H" tactic which applies functionalHugo Herbelin
2016-09-17Further "decide equality" tests on demand of Jason.Hugo Herbelin
2016-09-15Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Hugo Herbelin
2016-09-12Refolding: disable in 8.4 compat file, documentMatthieu Sozeau
2016-09-09no-refold patchPaul Steckler
2016-09-02Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-31Fix bug #5043: [Admitted] lemmas pick up section variables.Pierre-Marie Pédrot
2016-08-19Merge remote-tracking branch 'origin/pr/246' into v8.6Matthieu Sozeau
2016-08-18Merge remote-tracking branch 'github/bug4978' into v8.6Matthieu Sozeau
2016-08-18Fix an occurrence of deprecated eqn syntax in stdlib.Maxime Dénès
2016-08-17Fix #4978: priorities of Equivalence instancesMatthieu Sozeau
2016-07-18Replacing deprecated Implicit Arguments in prelude.Maxime Dénès
2016-07-18Remove the swap tactic from the prelude.Maxime Dénès
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 11:31:17 +0000