aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | | | | | | | | | Merge PR #890: Global universe declarationsGravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6266: Safe unmarshalling in the checkerGravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6301: [vernac] Couple of tweaks missing from previous PRs.Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6300: Clarify operation of sequences, fixes #6095Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6293: Check for Num lib if OCaml >= 4.06, fixes #6162Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #6007Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6287: Add merlin to default.nixGravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6210: More complete not-fully-applied error messages, #6145Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | * | | | | | | | | [default.nix] needs ncurses for the test-suiteGravatar Vincent Laporte2017-12-04
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | |
| | | | | | | | * | | | | | | | | | | | [vernac] Couple of tweaks missing from previous PRs.Gravatar Emilio Jesus Gallego Arias2017-12-04
| |_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular we must invalidate the state cache in the case of an exception.
| | | | | | | * | | | | | | | | | | | Adding a test for #6304 (bug with fix in notations).Gravatar Hugo Herbelin2017-12-03
| |_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | Remove redundant Zcase from the checker.Gravatar Pierre-Marie Pédrot2017-12-02
| |_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * | | | | | | | | | | | | | uninstall doc dir, not dev (which is not installed), #6007Gravatar Paul Steckler2017-12-01
| |_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | |
| | | * | | | | | | | | | | | | check for Num lib if OCaml >= 4.06, #6162Gravatar Paul Steckler2017-12-01
| | | | |_|_|_|_|_|_|/ / / / / | | | |/| | | | | | | | | | |
| | | | | * | | | | | | | | | clarify operation of sequences, #6095Gravatar Paul Steckler2017-12-01
| | | | |/ / / / / / / / / / | | | |/| | | | | | | | | |
| | | | | | * | | | | | | | Update CHANGESGravatar Matthieu Sozeau2017-12-01
| | | | | | | | | | | | | |
| | | | | | * | | | | | | | Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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.
| | | | | | * | | | | | | | [refman] Expand a little on global universes.Gravatar Matthieu Sozeau2017-12-01
| | | | | | | | | | | | | |
| | | | | | * | | | | | | | Tests for global universe declarationsGravatar Matthieu Sozeau2017-12-01
| | | | | | | | | | | | | |
| | | | | | * | | | | | | | Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
| |_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
| | | | | | * | | | | | | Documenting the -Q flag of coqchk.Gravatar Pierre-Marie Pédrot2017-12-01
| | | | | | | | | | | | |
* | | | | | | | | | | | | Merge PR #736: [ci] Test coqchk on the CompCert target.Gravatar Maxime Dénès2017-12-01
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6256: CI: better ocaml warning checksGravatar Maxime Dénès2017-12-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6276: Coqchk accepts filenamesGravatar Maxime Dénès2017-12-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6233: [proof] [api] Rename proof types in preparation for ↵Gravatar Maxime Dénès2017-12-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | functionalization.
* | | | | | | | | | | | | | | | Merge PR #1049: Remove obsolete localityGravatar Maxime Dénès2017-11-30
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6244: [lib] [api] Introduce record for `object_prefix`Gravatar Maxime Dénès2017-11-30
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | | | | | | | | [ci] Test coqchk on the CompCert target.Gravatar Théo Zimmermann2017-11-30
| | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵Gravatar Maxime Dénès2017-11-30
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | #3125)
| | | | | | | | * | | | | | | | | | Add merlin in the dependencies of nix-shell only.Gravatar Théo Zimmermann2017-11-30
| |_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.Gravatar Maxime Dénès2017-11-30
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as ↵Gravatar Maxime Dénès2017-11-30
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | instance.
| | | | | * | | | | | | | | | | | | | Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| |_|_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
| | | | | | | | | | | | | | * | | | Fix usage comment.Gravatar Théo Zimmermann2017-11-29
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | | | This script apparently uses bash-specific features.Gravatar Théo Zimmermann2017-11-29
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | | | Fix PR merge script.Gravatar Théo Zimmermann2017-11-29
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was still relying on the existence of user-configured /pr/.
| | | | * | | | | | | | | | | | | [lib] [api] Introduce record for `object_prefix`Gravatar Emilio Jesus Gallego Arias2017-11-29
| | | | | |_|_|_|_|_|_|_|_|_|_|/ | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
| | | | | | | | | | | * | | | | Forbid implicitly relative names in the checker.Gravatar Pierre-Marie Pédrot2017-11-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before this patch, passing a mere identifier (without dots) to the checker would make it consider it as implicitly referring to a relative name. For instance, if passed "foo", it would have looked for "Bar.foo.vo" and "Qux.foo.vo" if those files were in the loadpath. This was quite ad-hoc. We remove this "feature" and require the user to always give either a filename or a fully qualified logical name.
| | | | | | | | | | | * | | | | Mark the -I option in coqchk as deprecated and merge it with -Q.Gravatar Pierre-Marie Pédrot2017-11-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It is not doing the same thing as coqtop, and the corresponding coqtop semantics is irrelevant in the checker as the latter does not rely on ML code.
| | | | | | | | | | | * | | | | Add a -Q option to coqchck.Gravatar Pierre-Marie Pédrot2017-11-29
| | | | | | | |_|_|_|/ / / / / | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It has exactly the same effect as -R, because there is no such thing as implicit relativization for object files in coqchk, contrarily to what Require does in coqtop.
| | | | | * / | | | | | | | | [proof] [api] Rename proof types in preparation for functionalization.Gravatar Emilio Jesus Gallego Arias2017-11-29
| |_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular `Proof_global.t` will become a first class object for the upper parts of the system in a next commit.
* | | | | | | | | | | | | | Merge PR #6271: Add PR backport script.Gravatar Maxime Dénès2017-11-29
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6253: Fixing inconsistent associativity of level 10 in the table ↵Gravatar Maxime Dénès2017-11-29
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | of levels
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6199: [vernac] Uniformize type of vernac interpretation.Gravatar Maxime Dénès2017-11-29
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | | | | | coq_makefile: pass filenames to coqchkGravatar Ralf Jung2017-11-29
| | | | | | | | | | | | | | | | |
| | | | | | | | * | | | | | | | | Documenting the possibility to pass filenames to coqchk.Gravatar Pierre-Marie Pédrot2017-11-29
| | | | | | | | | | | | | | | | |
| | | | | | | | * | | | | | | | | Allow to pass physical files to coqchk.Gravatar Pierre-Marie Pédrot2017-11-29
| | | | | | | | | | | | | | | | |
| | | | | | * | | | | | | | | | | In injection/inversion, consider all template-polymorphic types as injectable.Gravatar Hugo Herbelin2017-11-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular singleton inductive types are considered injectable, even in the absence of the option "Set Keep Proof Equalities". This fixes #3125 (and #4560, #6273).