aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2017-05-31Merge PR#248: Adding eassert, eset, epose, etc.Maxime Dénès
2017-05-31Makefile.build: test-suite all = run + report, so don't report againGaëtan Gilbert
2017-05-31[travis] print failing test suite logs on failureGaëtan Gilbert
2017-05-31Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake ↵Maxime Dénès
(EDIT: for mutual fixpoints)
2017-05-31Tests for new specialize feature + CHANGES.Pierre Courtieu
2017-05-31Documenting the new behaviour of specialize.Pierre Courtieu
2017-05-31Make specialize smarter.Pierre Courtieu
Now when a partial with-binding is given the unsolved parameters are left quantified. A letin is added when mixing (fun x => ...) and with-bindings.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 04:35:17 +0000