aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-10-03Changed the statement of leb_not_le; shortened the proofRaphaël Monat
2017-10-03Ltac uses the new generic locatable API.Pierre-Marie Pédrot
2017-10-03Implementing a generic mechanism for locating named objects from Coq side.Pierre-Marie Pédrot
2017-10-03Moving the Ltac-specific part of the nametab to the Ltac plugin.Pierre-Marie Pédrot
For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit.
2017-10-03fix compilation on OCaml < 4.04Enrico Tassi
2017-10-03Merge branch 'master' of https://github.com/coq/coqRaphaël Monat
2017-10-03Add Qabs_Qinv: Qabs (/ q) == / (Qabs q).Raphaël Monat
2017-10-03Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x.Raphaël Monat
2017-10-03Add leb_not_le: (n <=? m) = false -> n > m.Raphaël Monat
2017-10-03Merge PR #1110: Mention requiring extraction/funind in CHANGESMaxime Dénès
2017-10-03Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags.Maxime Dénès
2017-10-03Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links.Maxime Dénès
2017-10-03Merge PR #1100: Avoid looping when searching for CoqProject.Maxime Dénès
2017-10-03Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵Maxime Dénès
proof for coqwc
2017-10-03Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).Maxime Dénès
2017-10-03Merge PR #1094: Fixing a little parsing bug with level 90 introduced in ↵Maxime Dénès
3e70ea9c.
2017-10-03Merge PR #1090: [ide] Avoid duplicate error printing (BZ#5583)Maxime Dénès
2017-10-03Merge PR #1084: After testing it in live, writing metas using an ↵Maxime Dénès
?INTERNAL#42 style is ugly
2017-10-03Remove GeoCoq from allowed failures.Théo Zimmermann
2017-10-03Fix GeoCoq build by using a shared CI configure.Théo Zimmermann
See also GeoCoq/GeoCoq#7.
2017-10-03Merge PR #1015: Adding a function to be typically used to pass values from ↵Maxime Dénès
an OCaml "when" clause to the r.h.s of the matching clause
2017-10-03Merge PR #1080: Remove some unused parts of the reference manual.Maxime Dénès
2017-10-03Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).Maxime Dénès
2017-10-03Merge PR #1072: Do not run Travis OS X packaging job on PRsMaxime Dénès
2017-10-03Merge PR #1040: Efficient fresh name generationMaxime Dénès
2017-10-03Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META fileMaxime Dénès
2017-10-03Merge PR #1019: Fix BZ#5655 by avoiding the creation of a cleaner thread for ↵Maxime Dénès
empty queues.
2017-10-03Merge PR #1012: Make a test for coq_makefile portable.Maxime Dénès
2017-10-03Merge PR #667: [vernac] Remove `Qed exporting` syntax.Maxime Dénès
2017-10-02Mention requiring extraction/funind in CHANGESTej Chajed
2017-10-01Abstracting away the implementation of value representations.Pierre-Marie Pédrot
2017-10-01Using Ltac2 native closures in some tactic APIs.Pierre-Marie Pédrot
2017-10-01Rolling up our own representation of clauses.Pierre-Marie Pédrot
2017-10-01Moving ML types used by Ltac2 to their proper interface.Pierre-Marie Pédrot
2017-09-30Abstracting away the primitive functions on valexpr datatype.Pierre-Marie Pédrot
2017-09-29Remove a failwith ""Gaëtan Gilbert
2017-09-29Remove unused Failure catchGaëtan Gilbert
Unused since dc57718e98289b5d71a0a942d6a063d441dc6a54 as far as I can tell.
2017-09-29Remove TODO comment (Evar.t is opaque)Gaëtan Gilbert
2017-09-29Cleanup suggest_bulletGaëtan Gilbert
2017-09-29Typo in coqdep manGaëtan Gilbert
2017-09-29Remove some duplication between Typeops and Nativenorm.Gaëtan Gilbert
2017-09-29start counting at 0...Ralf Jung
2017-09-29[ide] Avoid duplicate error printing (BZ#5583)Emilio Jesus Gallego Arias
See the discussion in the bug tracker, basically the STM delays the feedback error message to a point where CoqIDE has forgotten about the sentence, thus we were processing such errors in the generic case, printing them twice as the Fail case will also do it. We could indeed revert back to the 8.6 strategy for error (print always from Fail and ignore Feedback), however I feel that time will be better spent by fixing the STM than adding more CoqIDE workarounds.
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
2017-09-29Iris CI: use opam to determine std++ git commitRalf Jung
2017-09-28Remove trivial TODO comment (constants can't be template poly now).Gaëtan Gilbert
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
2017-09-27Remove catch-all try with in the beautifier.Théo Zimmermann
2017-09-27Beautifier gets its own formatter: fixes BZ#5704.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 11:12:52 +0000