aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-06Merge PR#600: Some factorizations of ltac interpretation functions between ↵Maxime Dénès
ssreflect and coq code
2017-06-06Merge PR#638: Fix bug #5360: anomalies in typeclass resolution outputMaxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-06Merge PR#723: [travis] [fiat] Test also fiat-core.Maxime Dénès
2017-06-05Merge PR#724: Move README.ci to markdownMaxime Dénès
2017-06-05Merge PR#726: [stm] Solve bug 5577 "STM branch name is incorrect with Time"Maxime Dénès
2017-06-05Merge PR#722: [printing] Remove duplicated printing function.Maxime Dénès
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ↵Maxime Dénès
a flag suspectingly renamed in a clearer way
2017-06-04Merge PR#526: solving implicit resolution in FunctionMaxime Dénès
2017-06-03[stm] Solve bug 5577 "STM branch name is incorrect with Time"Emilio Jesus Gallego Arias
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#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-01drop vo.itarget files and compute the corresponding the corresponding values ↵Matej Kosik
automatically instead
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-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-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-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-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-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.
2017-05-31Merge PR#700: make sure that "ocamllibdep" properly recognizes Ocaml that ↵Maxime Dénès
are composed from uppercase letters
2017-05-31Adding overlay for math-comp.Hugo Herbelin
2017-05-31Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
A priori considered to be a good programming style.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 17:10:07 +0000