aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-10-09Merge PR #1087: [stm] Switch to a functional APIMaxime Dénès
2017-10-09Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add ↵Maxime Dénès
Morphism` forms.
2017-10-09Merge PR #1134: Revert "Switch Travis to OSX 10.12 and Xcode 8.3.3."Maxime Dénès
2017-10-09Merge PR #1133: Fix hardcoded boot dependencies after #1041.Maxime Dénès
2017-10-09Merge PR #1132: TimeFileMaker.py: Allow trailing spacesMaxime Dénès
2017-10-09Merge PR #1115: Autolink to Github PRs from BugzillaMaxime Dénès
2017-10-09Merge PR #1114: Generic handling of nameable objects for pluginsMaxime Dénès
2017-10-09Merge PR #1109: Handle some misc todosMaxime Dénès
2017-10-09[deps] Move `Discharge` to `interp`Emilio Jesus Gallego Arias
More dependencies / linking fixes.
2017-10-09Merge PR #1086: [stm] [flags] Move document mode flags to the STM.Maxime Dénès
2017-10-09Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for ↵Maxime Dénès
printing-ony Notations
2017-10-09Merge PR #1117: [ci] Remove temporary bignums overlay.Maxime Dénès
2017-10-09Fix Travis OSX deploy conditional.Gaëtan Gilbert
IS is intended for testing nullity.
2017-10-09Include leading zeros in version infoTej Chajed
Fixes BZ#5779
2017-10-08Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey.Raphaël Monat
2017-10-08Removed leb_not_le (already existing as Nat.leb_nle)Raphaël Monat
2017-10-07Revert "Switch Travis to OSX 10.12 and Xcode 8.3.3."Théo Zimmermann
This reverts commit 587e556a909fcd2e1507a9230d9cdaffa3f9394e from PR #1024. This commit did not solve any issue at the time it was merged but made the macOS package we produce compatible only with macOS 10.12 and later.
2017-10-07Fix hardcoded boot dependencies after #1041.Gaëtan Gilbert
Specifically since e88dfedd99a84e9e375f3583be6fd1de3de36c72. There seem to have been no actual errors due to this, only ocaml complaining about missing .cmi files.
2017-10-07travis: remove the overlay on bignumsPierre Letouzey
This overlay is now useless (change pushed upstream in bignums) and moreover does not contain my commit making bignums resilient to PR#768.
2017-10-07Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768)Pierre Letouzey
2017-10-06[stm] Switch to a functional APIEmilio Jesus Gallego Arias
We make the Stm API functional over an opaque `doc` type. This allows to have a much better picture of what the toplevel is doing; now almost all users of STM private data are marked by typing. For now only, the API is functional; a PR switching the internals should come soon thou; however we must first fix some initialization bugs. Due to some users, we modify `feedback` internally to include a "document id" field; we don't expose this change in the IDE protocol yet.
2017-10-06[stm] [flags] Move document mode flags to the STM.Emilio Jesus Gallego Arias
We move toplevel/STM flags from `Flags` to their proper components; this ensures that low-level code doesn't depend on them, which was incorrect and source of many problems wrt the interfaces. Lower-level components should not be aware whether they are running in batch or interactive mode, but instead provide a functional interface. In particular: == Added flags == - `Safe_typing.allow_delayed_constants` Allow delayed constants in the kernel. - `Flags.record_aux_file` Output `Proof using` information from the kernel. - `System.trust_file_cache` Assume that the file system won't change during our run. == Deleted flags == - `Flags.compilation_mode` - `Flags.batch_mode` Additionally, we modify the STM entry point and `coqtop` to account for the needed state. Note that testing may be necessary and the number of combinations possible exceeds what the test-suite / regular use does. The next step is to fix the initialization problems [c.f. Bugzilla], which will require a larger rework of the STM interface.
2017-10-06[coqtop] Don't reset coqinit internal variables after initialization.Emilio Jesus Gallego Arias
We remove `init_library_roots` as there is no point in resetting this internal variable. Its only user is `init_load_path` and this function is not meant (and is not) idempotent now.
2017-10-06Merge PR #1127: Shorten the .gitattributes file.Maxime Dénès
2017-10-06Merge PR #1118: Extraction : minor support stuff for the new Extraction ↵Maxime Dénès
Compute plugin
2017-10-06Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵Maxime Dénès
"_something")
2017-10-06Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ↵Maxime Dénès
inductive definition)
2017-10-06Merge PR #1125: [pp] Minor optimization in `Pp.t` construction and gluing.Maxime Dénès
2017-10-06Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly ↵Maxime Dénès
BZ#4852)
2017-10-06Merge PR #1128: GitLab CI: make all_stdlib.v in build jobMaxime Dénès
2017-10-06Merge PR #1130: Fix copyright info in reference manual.Maxime Dénès
2017-10-06Merge PR #1131: Clean-up xml protocol docMaxime Dénès
2017-10-06Merge PR #1129: 8.7+beta2 CHANGESMaxime Dénès
2017-10-06Merge PR #1123: [ci] Remove deploy to GitHub of OS X package.Maxime Dénès
2017-10-06TimeFileMaker.py: Allow trailing spacesJason Gross
This allows the timing aggregation scripts to handle logs from Travis, which, for some reason, seems to insert trailing spaces.
2017-10-06Extract changes to the XML protocol from its docThéo Zimmermann
2017-10-06Make the XML protocol doc more version-independentThéo Zimmermann
2017-10-06Fix copyright info in reference manual.Théo Zimmermann
Also simplifies the way it is presented (no need to be overly precise).
2017-10-068.7+beta2 CHANGESThéo Zimmermann
2017-10-05[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Emilio Jesus Gallego Arias
The manual has long stated that these forms are deprecated. We add a warning for them, as indeed `Add Morphism` is an "proof evil" [*] command, and we may want to remove it in the future. We've also fixed the stdlib not to emit the warning. [*] https://ncatlab.org/nlab/show/principle+of+equivalence
2017-10-05romega: takes advantage of context variables with bodyPierre Letouzey
When a context variable x is of the form "x := body : Z", romega is now made aware of this body. Technically, we reify an equation x = body, and push a corresponding (eq_refl x) as argument of the final do_omega. See also the previous commit adding this same feature to omega (fixing bug 142).
2017-10-05Omega now aware of context variables with bodies (in type Z or nat) (fix bug ↵Pierre Letouzey
148) For compatibility, this extra feature of omega could be disabled via Unset Omega UseLocalDefs. Caveat : for now, real let-ins inside goals or hyps aren't handled, use some "cbv zeta" reduction if you want to get rid of them. And context definitions whose types aren't Z or nat are ignored, some manual "unfold" are still mandatory if expanding these definitions will help omega.
2017-10-05Merge PR #1069: Improve support for -w optionsMaxime Dénès
2017-10-05Merge PR #1081: Mini fix at improving the cannot unify error messageMaxime Dénès
2017-10-05Fix typo in INSTALLMaxime Dénès
2017-10-05Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Maxime Dénès
to escape non-UTF-8 file names)
2017-10-05Merge PR #1093: [doc] Update INSTALL to match reality.Maxime Dénès
2017-10-05Merge PR #1107: Add coqwc tests to test suiteMaxime Dénès
2017-10-05GitLab CI: make all_stdlib.v in build jobGaëtan Gilbert
2017-10-05Merge PR #1106: Fix beautifierMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 10:53:49 +0000