aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-08Adding a test case as requested in bug 5205.Théo Zimmermann
2017-06-08Remove overlay.Maxime Dénès
2017-06-08Merge PR#652: Put all plugins behind an "API".Maxime Dénès
2017-06-07Update .gitignoreJason Gross
2017-06-07[stm] More fixes for nested commands [bugzilla 5589]Emilio Jesus Gallego Arias
2017-06-07Fix documentation of Typeclasses eauto :=Théo Zimmermann
2017-06-07completing a sentence in a commentMatej Košík
2017-06-07[kernel] Improve proof using message, fixes bugzilla #3613Emilio Jesus Gallego Arias
2017-06-07add overlaysMatej Košík
2017-06-07Put "ssreflect" behind "API".Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-07Merge PR#698: Trunk miscMaxime Dénès
2017-06-07Merge PR#717: [proof] Deprecate "proof mode" APIMaxime Dénès
2017-06-07Merge PR#669: Ssr mergeMaxime Dénès
2017-06-06Overlay.Maxime Dénès
2017-06-06Merge the ssr plugin.Maxime Dénès
2017-06-06Remove some overlays.Maxime Dénès
2017-06-06Merge PR#623: Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-06Overlays.Maxime Dénès
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
2017-06-06Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a ↵Maxime Dénès
short econstr-cleaning of record.ml
2017-06-06Merge PR#728: A few typos.Maxime Dénès
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-05Univs: fix bug #5365, generation of u+k <= v constraintsMatthieu Sozeau
Use an explicit label ~algebraic for make_flexible_variable as well.
2017-06-04Added support for a side effect on constants in reduction functions.Thomas Sibut-Pinote
This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-27 14:53:58 +0000