aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-11-27Merge PR #6207: [stm] Allow delayed constant in interactive mode.Maxime Dénès
2017-11-27Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp.Maxime Dénès
2017-11-27Merge PR #6241: [lib] Generalize Control.timeout type.Maxime Dénès
2017-11-27Merge PR #6228: Make byte on gitlab.Maxime Dénès
2017-11-27Merge PR #6226: Enhance votourMaxime Dénès
2017-11-27Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffsMaxime Dénès
2017-11-27Merge PR #6041: Protecting the printing of filenames with spaceMaxime Dénès
2017-11-27Merge PR #6227: Linter: do not lint untracked files.Maxime Dénès
2017-11-24[lib] Generalize Control.timeout type.Emilio Jesus Gallego Arias
We also remove some internal implementation details from the mli file, there due historical reasons.
2017-11-24Merge PR #6231: Fix link to Recursive Make Considered HarmfulMaxime Dénès
2017-11-24Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRingMaxime Dénès
2017-11-24Merge PR #486: Make some functions on terms more robust w.r.t new term ↵Maxime Dénès
constructs.
2017-11-24Fix deprecated syntax warning from vernacextend.mlp.Gaëtan Gilbert
2017-11-24Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionMaxime Dénès
2017-11-24Make byte on gitlab.Gaëtan Gilbert
Hopefully this will stop the intermittent test-suite/coq-makefile/findlib-package failures.
2017-11-24Update PR filter used by RM.Maxime Dénès
2017-11-24Merge PR #6197: [plugin] Remove LocalityFixme über hack.Maxime Dénès
2017-11-23Unify style of comments in file CUnix.Hugo Herbelin
2017-11-23Quote file names which have spaces in "Print LoadPath".Hugo Herbelin
The primary concern is for clarity of reading. May it affects tools which would parse the output of "Print LoadPath"? Presumably, these tools would not support file names with spaces already, so this may have no impact.
2017-11-23Add a function to surround filenames containing a space with quotes.Hugo Herbelin
2017-11-23Surrounding a few places printing file names with quotes when a space occurs.Hugo Herbelin
2017-11-23Make one more function robust in term_dnet.mlMaxime Dénès
Was actually forgotten in native-coq.
2017-11-23Make some functions on terms more robust w.r.t new term constructs.Maxime Dénès
Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
2017-11-23Merge PR #6167: Fixing factorization of recursive notations with an atomic ↵Maxime Dénès
separator
2017-11-23Merge PR #6203: Fix universe polymorphic Program obligations.Maxime Dénès
2017-11-23Merge PR #6186: [api] Miscellaneous consolidation.Maxime Dénès
2017-11-23Merge PR #6221: Add PR filter used by RM to the contributing guide.Maxime Dénès
2017-11-23Fix link to Recursive Make Considered HarmfulGaëtan Gilbert
2017-11-23Add PR filter used by RM to the contributing guide.Maxime Dénès
2017-11-23Linter: do not lint untracked files.Gaëtan Gilbert
2017-11-23Adding ad hoc overlay for sf/vfa.Hugo Herbelin
2017-11-23Recognizing Z in romega up to conversion.Hugo Herbelin
2017-11-23Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Hugo Herbelin
Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717.
2017-11-23Fixing a 8.7 regression of ring_simplify in ArithRing.Hugo Herbelin
With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191).
2017-11-23Truncate strings in votour to 1024 characters.Pierre-Marie Pédrot
Making it bigger is kind of useless, takes time and clutters the output for no real advantage.
2017-11-23Merge PR #6200: Remove pidentref grammar entry.Maxime Dénès
2017-11-23Merge PR #1092: [stm] [doc] Add some documentation to obscure AsyncTaskQueueMaxime Dénès
2017-11-23Bypass int and string representation in votour when it's incorrect.Pierre-Marie Pédrot
2017-11-23Tail-recursive list traversal in votour.Pierre-Marie Pédrot
2017-11-23Merge PR #6123: Nix fileMaxime Dénès
2017-11-23Merge PR #6189: Disable whitespace linter for .out files.Maxime Dénès
2017-11-23Merge PR #6187: Check findlib version in configure (fix #4270).Maxime Dénès
2017-11-23Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Maxime Dénès
2017-11-22[plugin] Remove LocalityFixme über hack.Emilio Jesus Gallego Arias
To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it.
2017-11-22[plugin] Encapsulate modifiers to vernac commands.Emilio Jesus Gallego Arias
This is a continuation on #6183 and another step towards a more functional interpretation of commands. In particular, this should allow us to remove the locality hack.
2017-11-22Add test-suite tests for timing scriptsJason Gross
These work on precomputed build logs (in this case, from a recent partial build of fiat-crypto). They are meant to serve as human-readable sanity checks of output format. Separate out the sane bits of template/init.sh from the ones messing with directory structure (which are fragile and make assumptions about where the calling script is sourcing it from). N.B. The test-suite removes all *.log files, so we use *.log.in. N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile, because coqc, on Windows, doesn't handle cygwin paths passed via -coqlib, and `pwd` gives cygwin paths. N.B. We have .gitattributes to satisfy the linter (as per https://github.com/coq/coq/pull/6149#issuecomment-346410990)
2017-11-22Update TimeFileMaker.py to correctly sort timing diffsJason Gross
Previously, it was reverse-ordering timing diffs.
2017-11-22Implement a tail-recursive traversal of the object in votour.Pierre-Marie Pédrot
2017-11-22[api] A few more minor deprecation notices.Emilio Jesus Gallego Arias
Note the problem with `create_evar_defs`.
2017-11-22[api] Re-enable deprecation warnings.Emilio Jesus Gallego Arias
With a bit of care we can enable full deprecation warnings again in this funny file.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:32:09 +0000