aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-10-05Extraction: reduce eta-redexes whose cores are atomic (solves indirectly ↵Pierre Letouzey
BZ#4852) This code simplification isn't that important, but it can trigger further simplifications elsewhere, see for instance BZ#4852. NB: normally, the extraction favors eta-expanded forms, since that's the usual way to avoid issues about '_a type variables that cannot be generalized. But the atomic eta-reductions done here shouldn't be problematic (no applications put outside of functions).
2017-10-05Shorten the .gitattributes file.Théo Zimmermann
.dir-locals.el can be useful for users of the tarballs as well, and TODO doesn't exist anymore.
2017-10-05[pp] Minor optimization in `Pp.t` construction and gluing.Emilio Jesus Gallego Arias
The typical Coq `Pp.t` document contains a lot of "gluing" which produces efficient structures but it is quite painful in serialization. We optimize a common document building case so we don't create as much glue nodes as with the "naive" strategy, and without incurring in the large performance cost full flattening would produce. This is a temporal fixup, see #505 for more context on the discussion and medium-term plans.
2017-10-05[ci] Remove deploy to GitHub of OS X package.Théo Zimmermann
This is inconvenient because it can only be tested on tags and it didn't work for V8.7+beta1.
2017-10-05Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Hugo Herbelin
2017-10-05Distinguishing pseudo-letters out of the set of unicode letters.Hugo Herbelin
This includes _ and insecable space which can be used in idents and this allows more precise heuristics.
2017-10-05Fixing typos in comments of unicode.ml.Hugo Herbelin
2017-10-05Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).Hugo Herbelin
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
This allows e.g. the following to work: Reserved Notation "* a" (at level 70). Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m). We seize this opportunity to make main calls to Metasyntax to depend on an arbitrary env rather than on Global.env. Incidentally, this fixes a little coqdoc bug in classifying the inductive type referred to in the "where" clause.
2017-10-04Merge PR #1006: fix: ssrmatching and primitive projectionsMaxime Dénès
2017-10-04Merge PR #1078: Report missing arguments in error messageMaxime Dénès
2017-10-04Extraction : minor support stuff for the new Extraction Compute pluginPierre Letouzey
See https://github.com/letouzey/extraction-compute for more details
2017-10-04Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677]Maxime Dénès
2017-10-04[ci] Remove temporary bignums overlay.Théo Zimmermann
2017-10-04Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).Maxime Dénès
2017-10-03add coqwc testsPaul Steckler
2017-10-03autolink to Github PRs from BugzillaPaul Steckler
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 13:25:44 +0000