aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-10-12Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans.Raphaël Monat
2017-10-12Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or ↵Maxime Dénès
directory` on every execution
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-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-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-07Implementing the Constr.in_context function.Pierre-Marie Pédrot
2017-10-07Remove unused warnings.Pierre-Marie Pédrot
2017-10-07Fix coq/ltac2#30: Compilation broken since -safe-string PR got merged.Pierre-Marie Pédrot
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-27 10:36:01 +0000