aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-12-07Merge PR #873: New strategy based on open scopes for deciding which notation ↵Maxime Dénès
to use among several of them
2017-12-07Merge PR #6142: Single quotes break on WindowsMaxime Dénès
2017-12-07Merge PR #6277: Qualified import in coqchkMaxime Dénès
2017-12-07[configure] fix spelling mistakeVincent Laporte
2017-12-07Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding)Maxime Dénès
2017-12-07Merge PR #6321: Use preference for ocamlfind in configureMaxime Dénès
2017-12-07Merge PR #6316: Correct typoMaxime Dénès
2017-12-07Merge PR #6309: [default.nix] needs ncurses for the test-suiteMaxime Dénès
2017-12-07Merge PR #6303: Remove redundant Zcase from the checker.Maxime Dénès
2017-12-06Additional rewrite lemmas on Ensembles, in Powerset_factsJoachim Breitner
2017-12-06Getting rid of pf_is_matching in Funind.Pierre-Marie Pédrot
2017-12-06Getting rid of the Update constructor in Reductionops.Pierre-Marie Pédrot
This was dead code, probably due to the fact it was once shared with the kernel stack type.
2017-12-06Getting rid of the Shift constructor in Reductionops.Pierre-Marie Pédrot
It was actually not used. The only place generating one was easily writable without it.
2017-12-06issue deprecation warning for "Ocaml"Paul Steckler
2017-12-06Overlay for Equations.Gaëtan Gilbert
2017-12-06Linter: skip PRs older than the linter.Gaëtan Gilbert
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c].
2017-12-05Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.Hugo Herbelin
This fixes #6286 as suggested by PMP. See details of discussion at #6286.
2017-12-05Rename update to set, fixes #6196Paul Steckler
2017-12-05use preference for ocamlfindPaul Steckler
2017-12-05use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguagePaul Steckler
2017-12-05Don't Add LoadPath on CoqIDE startup, #6153Paul Steckler
2017-12-05Correct typoMartin Vassor
2017-12-05[default.nix] explain ncurses dependencyVincent Laporte
2017-12-05Merge PR #890: Global universe declarationsMaxime Dénès
2017-12-05Merge PR #6266: Safe unmarshalling in the checkerMaxime Dénès
2017-12-05[configure] adds a `select_command` functionVincent Laporte
2017-12-05Merge PR #6301: [vernac] Couple of tweaks missing from previous PRs.Maxime Dénès
2017-12-05Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).Maxime Dénès
2017-12-05Merge PR #6300: Clarify operation of sequences, fixes #6095Maxime Dénès
2017-12-05Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Maxime Dénès
2017-12-05Merge PR #6293: Check for Num lib if OCaml >= 4.06, fixes #6162Maxime Dénès
2017-12-05Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #6007Maxime Dénès
2017-12-05Merge PR #6287: Add merlin to default.nixMaxime Dénès
2017-12-05Merge PR #6210: More complete not-fully-applied error messages, #6145Maxime Dénès
2017-12-04[configure] fix detection of `md5sum`Vincent Laporte
2017-12-04[default.nix] needs ncurses for the test-suiteVincent Laporte
2017-12-04[vernac] Couple of tweaks missing from previous PRs.Emilio Jesus Gallego Arias
In particular we must invalidate the state cache in the case of an exception.
2017-12-03Adding a test for #6304 (bug with fix in notations).Hugo Herbelin
2017-12-02Remove redundant Zcase from the checker.Pierre-Marie Pédrot
This was redundant with ZcaseT, the only difference lying in the use or not of fclosures for substerms. This code was removed from the kernel in commit f2f805ed, we finish the work in the checker now.
2017-12-02[kernel] Patch allowing to disable VM reduction.Emilio Jesus Gallego Arias
The patch has three parts: - Introduction of a configure flag `-bytecode-compiler (yes|no)` (due to static initialization this is a configure-time option) - Installing the hooks that register the VM with the pretyper and the kernel conditionally on the flag. - Replacing the normalization function in `Redexpr` by compute if the VM is disabled. We also rename `Coq_config.no_native_compiler` to `native_compiler` and `Flags.native_compiler` to `output_native_objects` [see #4607].
2017-12-01uninstall doc dir, not dev (which is not installed), #6007Paul Steckler
2017-12-01check for Num lib if OCaml >= 4.06, #6162Paul Steckler
2017-12-01clarify operation of sequences, #6095Paul Steckler
2017-12-01Fix #6297: handle constraints like (u+1 <= Set/Prop)Gaëtan Gilbert
2017-12-01proposed fix for issue #3213: extra variable m in Lt.S_predfredokun
2017-12-01Update CHANGESMatthieu Sozeau
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
- Regularly declared for for polymorphic constants - Declared globally for monomorphic constants. E.g mono@{i} := Type@{i} is printed as mono@{mono.i} := Type@{mono.i}. There can be a name clash if there's a module and a constant of the same name. It is detected and is an error if the constant is first but is not detected and the name for the constant not registered (??) if the constant comes second. Accept VarRef when registering universe binders Fix two problems found by Gaëtan where binders were not registered properly Simplify API substantially by not passing around a substructure of an already carrier-around structure in interpretation/declaration code of constants and proofs Fix an issue of the stronger restrict universe context + no evd leak This is uncovered by not having an evd leak in interp_definition, and the stronger restrict_universe_context. This patch could be backported to 8.7, it could also be triggered by the previous restrict_context I think.
2017-12-01[refman] Expand a little on global universes.Matthieu Sozeau
2017-12-01Tests for global universe declarationsMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 05:47:48 +0000