aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-10-18[travis] Add flambda testing.Emilio Jesus Gallego Arias
2017-10-16Merge PR #1153: [stdlib] Fix warnings on deprecated `Add Setoid`Maxime Dénès
2017-10-16Merge PR #1152: Fix BZ#5785 (make install -j broken)Maxime Dénès
2017-10-15[stdlib] Fix warnings on deprecated `Add Setoid`Emilio Jesus Gallego Arias
The test suite cases are preserved until the feature is actually removed.
2017-10-13Fix some more missing mkdir lines to Makefile.ideJason Gross
2017-10-13Fix BZ#5785 (make install -j broken)Jason Gross
This adds back `$(MKDIR) $(FULLCOQLIB)/toploop`, which was lost between 8.6 and 8.7.
2017-10-13Merge PR #1103: Take Suggest Proof Using outside the kernel.Maxime Dénès
2017-10-12Merge PR #1089: [stm] [toplevel] Move delicate state initialization to the ↵Maxime Dénès
STM (BZ#5556)
2017-10-12Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or ↵Maxime Dénès
directory` on every execution
2017-10-11Merge PR #1054: Restoring test on ident validity while browsing directory ↵Maxime Dénès
structure.
2017-10-11Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵Maxime Dénès
execution
2017-10-11[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Emilio Jesus Gallego Arias
We move delicate library/module instillation code to the STM so the API guarantees that the first state snapshot is correct. That was not the case in the past, which meant that the STM cache was unsound in batch mode, however we never used its contents due to not backtracking to the first state. This provides quite an improvement in the API, however more work is needed until the codepath is fully polished. This is a critical step towards handling the STM functionally.
2017-10-11Merge PR #1143: fix coq_makefile on cygwinMaxime Dénès
2017-10-10Stm.get_hint_ctx: remove unused Str.splitGaëtan Gilbert
With suggest proof using out of the kernel the format of context_used in .aux is just the list of ids wanted by get_hint_ctx. (split x s when x doesn't appear in s just returns the singleton list [s])
2017-10-10Parse [Proof using Type] without translating Type to an id.Gaëtan Gilbert
2017-10-10Use a nice printer for constant names in Suggest Proof Using.Gaëtan Gilbert
2017-10-10Code factorization Vernacentries.interp on VernacProof.Gaëtan Gilbert
2017-10-10[vernac] Remove "Proof using" hacks from parser.Emilio Jesus Gallego Arias
We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.
2017-10-10Take Suggest Proof Using outside the kernel.Gaëtan Gilbert
Also add an output test for Suggest Proof Using. This changes the .aux output: instead of getting a key >context_used "$hyps;$suggest" where $hyps is a list of the used hypotheses and $suggest is the ;-separated suggestions (or the empty string if Suggest Proof Using is unset), there is a key >context_used "$hyps" and if Suggest Proof Using is set also a key >suggest_proof_using "$suggest" For instance instead of 112 116 context_used "B A;A B;All" we get 112 116 context_used "B A" 112 116 suggest_proof_using "A B;All"
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 03:46:11 +0000