aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)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
Don't know if compare_cont is very useful to use, but, at least, these extensions make sense.
2017-03-03Compatibility of iff wrt not and imp.Hugo Herbelin
This completes the series and cannot hurt.
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
Hurkens.v by dropping the artificial need for monad laws. Tactic eauto decided to be dependent on the laws but there is a shorter proof without them. [Interestingly, eauto is not able to find the short proof. This is a situation of the form subgoal 1: H : ?A |- P x subgoal 2: H : M ?A |- M (forall x, P x) where addressing the second subgoal would find the right instance of ?A, but this instance is too hard to find by addressing first the first subgoal.]
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
Without this change, coqtop complains that I need to require Coq.Init.Logic to use [replace ... with ... by ...].
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
2017-02-15Added some theory on powerRZ.Thomas Sibut-Pinote
For this, I used a new inductive type Z_spec to reason on Z.
2017-01-30Proof clean-up.Théo Zimmermann
- Do not use induction/elim when not necessary: use destruct or destructive intro-pattern instead. - Do not use heavy automation when lightweight automation is enough. - Prefer shorter proofs when it does not hinder readability. - Do not rely on automatically generated names. - Use bullets.
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
because P:U->Prop implies P:U->Type, the new statement is strictly more useful. No change was needed to the proof.
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-24Fix some documentation typos.Guillaume Melquiond
Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
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
Was PR#331: Solve_constraints and Set Use Unification Heuristics
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
Was PR#336: Remove v62
2016-11-04Silence option deprecation warnings in the compat fileJason Gross
Some options are expected to be deprecated
2016-10-24Remove v62 from stdlib.Théo Zimmermann
This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore.
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
I've messed up with parts of the compatibility files I had to commit.
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
A file was introduced by mistake in theories/Logic.
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
if_then_else definition does not account for multi success tactics. tryif_then_else is a primitive tactical with the expected behavior.
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
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files.
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
Importing VectorNotations breaks `; []`. So we make sure it's not imported by defualt. Some files might be required to `Import VectorDef.VectorNotations` rather than just `Import VectorNotations`.
2016-09-26Fix bug #4785 (use [ ] for vector nil)Jason Gross
Also delimit vector_scope with vector, so that people can write %vector without having to delimit it themselves.
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-09-25 02:07:15 +0000