aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-10-11Remove GeoProof support.Maxime Dénès
Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
2017-10-11Merge PR #1054: Restoring test on ident validity while browsing directory ↵Maxime Dénès
structure.
2017-10-11Merge PR #1143: fix coq_makefile on cygwinMaxime Dénès
2017-10-10Merge PR #1140: Fix Travis OSX deploy conditional.Maxime Dénès
2017-10-10Fix BZ#5780: coq_makefile broken under CygwinRalf Jung
2017-10-10Merge PR #540: [configure] Support for flambda flags.Maxime Dénès
2017-10-10Merge PR #1116: Updating citing Coq in FAQ.Maxime Dénès
2017-10-10Updating citing Coq in FAQ.Hugo Herbelin
2017-10-10Restoring test on ident validity while browsing directory structure.Hugo Herbelin
The test was abandoned at the time of merging subdirectory browsing between coqdep and coqtop, and to limit at the same time the dependency of coqdep in files such as unicode.cmo. But checking ident validity speeds up browsing in arbitrary directory structure and we restore it for this reason. (One could also say that browsing arbitrary directory structures is not intended, but in practice this may happen, as e.g. reported in BZ#5734.)
2017-10-10Adding headers to segmenttree.{ml,mli}.Hugo Herbelin
2017-10-10Merge PR #1137: Include leading zeros in version infoMaxime Dénès
2017-10-10Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Maxime Dénès
2017-10-10Merge PR #1053: [deps] Move `Discharge` to `interp`Maxime Dénès
2017-10-10Merge PR #1067: Iris CI: use opam to install dependenciesMaxime Dénès
2017-10-10[flambda] [native] Pass `-Oclassic` to the native compiler.Emilio Jesus Gallego Arias
This seems a safe choice as of today, but more advanced users would like to tweak it, or we could even refine it by a configure option if desired.
2017-10-10[configure] Support for flambda flags.Emilio Jesus Gallego Arias
We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 13:47:23 +0000