aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-04A few typos.Hugo Herbelin
2017-06-04Ensure that warnings new from ocaml > 4.01 remains silent.Hugo Herbelin
Indeed, 8.6 is announced to be compilable with 4.01.0 and it is convenient not seeing warnings about which nothing can be done. Remove deprecation warnings new from ocaml 4.03, as well as warning 52. This is a partial cherry-pick of a77734ad6.
2017-06-04configure: avoid deprecated warningsPierre Letouzey
2017-06-04Fixing an inconsistency between configure and configure.ml.Hugo Herbelin
The shell script configure was assuming the existence of option -camldir which was removed in 333d41a9.
2017-06-04Merge PR#526: solving implicit resolution in FunctionMaxime Dénès
2017-06-03[tactics] Fix summary registration of global hint variable.Emilio Jesus Gallego Arias
It looks like `Class_tactics` forgot to register a couple of global variables with the summary, thus creating problems on backtracking. Fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5578
2017-06-03[stm] Solve bug 5577 "STM branch name is incorrect with Time"Emilio Jesus Gallego Arias
2017-06-02Add an overlay for coq-dpdgraph for 8.7Jason Gross
2017-06-02Make coq-dpdgraph allow-failJason Gross
2017-06-02Add coq-dpdgraph CIJason Gross
2017-06-02Use Names.Constant.printJason Gross
As per https://github.com/coq/coq/pull/716#discussion_r119963405
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
2017-06-02Don't double up on periods in anomaliesJason Gross
We don't want "Anomaly: Returned a functional value in a type not recognized as a product type.. Please report at http://coq.inria.fr/bugs/." but instead "Anomaly: Returned a functional value in a type not recognized as a product type. Please report at http://coq.inria.fr/bugs/."
2017-06-02Merge PR#720: Reformat Makefile.ciMaxime Dénès
2017-06-02Move README.ci to markdownThéo Zimmermann
The file was already (mostly) following Markdown syntax so we just take advantage of this by moving to a .md extension.
2017-06-02Merge PR#708: [ide] Correct merging error.Maxime Dénès
2017-06-02Merge PR#691: [travis] Add OSX test-suite checking.Maxime Dénès
2017-06-02Merge PR#705: Fix bug #5019 (looping zify on dependent types)Maxime Dénès
2017-06-02Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.Maxime Dénès
2017-06-02Merge PR#499: Drop all "theories/*/vo.itarget" files and compute the ↵Maxime Dénès
corresponding information automatically.
2017-06-02Merge PR#515: extract "plugins/micromega/micromega.ml{,i}" files from ↵Maxime Dénès
"plugins/micromega/MExtraction.v"
2017-06-02Merge PR#711: [gitlab] Artifact test suite logs on failure.Maxime Dénès
2017-06-02[travis] [fiat] Test also fiat-core.Emilio Jesus Gallego Arias
I didn't rename the test file to `fiat` as IMHO it is not worth the noise.
2017-06-01[travis] Add OSX test-suite checking.Maxime Dénès
This is a first step towards getting Travis build our OSX package, but is also useful immediately (c.f. the recent breakage of the coq_makefile test-suite under OSX).
2017-06-01Test-suite: do not test native compiler if disabled by configure.Maxime Dénès
2017-06-01solving implicit resolution in FunctionJulien Forest
2017-06-01mention 'make world' without 'byte' in CHANGES + 2 minor suggestionsPierre Letouzey
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ↵Matej Kosik
automatically instead
2017-06-01test-suite/coq-makefile: we do not build byte file by default anymorePierre Letouzey
2017-06-01Merge PR#449: make specialize smarter (bug 5370).Maxime Dénès
2017-06-01Merge PR#670: Postponing of universe constraints unification in term equality.Maxime Dénès
2017-06-01[emacs] [toplevel] Make emacs flag local to the toplevel.Emilio Jesus Gallego Arias
We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
2017-06-01Merge PR#696: Trunk+cleanup constr of globalMaxime Dénès
2017-06-01Merge PR#631: Fix bug #5255Maxime Dénès
2017-06-01Remove a post merge warning.Maxime Dénès
2017-06-01Merge PR#561: Improving the Name APIMaxime Dénès
2017-06-01Fix coq_makefile uninstall target under OSX.Maxime Dénès
2017-06-01Bump year in headers.Maxime Dénès
2017-06-01Merge PR#694: Fixing #5523 (missing support for complex constructions in ↵Maxime Dénès
recursive notations) (bis)
2017-06-01Break circular dependency in MExtractionJason Gross
Described in https://github.com/coq/coq/pull/515#discussion_r119230833
2017-06-01a solution that works also with make 3.81Matej Kosik
2017-06-01extract "plugins/micromega/micromega.ml{,i}" files from ↵Matej Kosik
"plugins/micromega/MExtraction.v"
2017-06-01Fix bug #5019 (looping zify on dependent types)Jason Gross
This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019), "[zify] loops on dependent types"; before, we would see a `Z.of_nat (S ?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on this. This may not be the "right" fix (there may be cases where `zify` should succeed where it still fails with this change), but this is a pure bugfix in the sense that the only places where it changes the behavior of `zify` are the places where, previously, `zify` looped forever.
2017-06-01Add opened bug 5019Jason Gross
2017-06-01Merge PR#710: Add test-suite checks for coqchk with constraintsMaxime Dénès
2017-06-01[printing] Remove duplicated printing function.Emilio Jesus Gallego Arias
It seems there were 4 copies of the same function in the code base.
2017-06-01Merge PR#704: Fix empty parentheses display in test-suiteMaxime Dénès
2017-05-31Merge PR#701: [readlink -f] doesn't work on OSXMaxime Dénès
2017-05-31Reformat Makefile.ciJason Gross
2017-05-31[proof] Deprecate "proof mode" APIEmilio Jesus Gallego Arias
Any users of this API should coordinate with the ongoing work in PRs numbered #459 and #566.
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-23 02:03:40 +0000