aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2017-05-31Merge PR#700: make sure that "ocamllibdep" properly recognizes Ocaml that ↵Maxime Dénès
are composed from uppercase letters
2017-05-31Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with ↵Maxime Dénès
section variables.
2017-05-31removing duplicate line from "tools/CoqMakefile.in"Matej Košík
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.
2017-05-31Renaming allow_patvar flag of intern_gen into pattern_mode.Hugo Herbelin
This highlights that this is a binary mode changing the interpretation of "?x" rather than additionally allowing patvar.
2017-05-31Overlay for math-comp.Hugo Herbelin
2017-05-31Factorizing interp_gen through a function interpreting glob_constr.Hugo Herbelin
The new function is interp_glob_closure which is basically a renaming and generalization of interp_uconstr. Note a change of semantics that I could however not observe in practice. Formerly, interp_uconstr discarded ltac variables bound to names for interning, but interp_constr did not. Now, both discard them. We also export the new interp_glob_closure.
2017-05-31Splitting interp_open_constr into two variants, with or without type classes.Hugo Herbelin
This simplifies the API as before, inference of instances of type classes was iff a type constraint was given. We then export these both versions of interp_open_constr.
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-27 19:00:41 +0000