| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-06 | Merge PR #1127: Shorten the .gitattributes file. | Maxime Dénès | |
| 2017-10-06 | Merge PR #1118: Extraction : minor support stuff for the new Extraction ↵ | Maxime Dénès | |
| Compute plugin | |||
| 2017-10-06 | Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵ | Maxime Dénès | |
| "_something") | |||
| 2017-10-06 | Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ↵ | Maxime Dénès | |
| inductive definition) | |||
| 2017-10-06 | Merge PR #1125: [pp] Minor optimization in `Pp.t` construction and gluing. | Maxime Dénès | |
| 2017-10-06 | Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly ↵ | Maxime Dénès | |
| BZ#4852) | |||
| 2017-10-06 | Merge PR #1128: GitLab CI: make all_stdlib.v in build job | Maxime Dénès | |
| 2017-10-06 | Merge PR #1130: Fix copyright info in reference manual. | Maxime Dénès | |
| 2017-10-06 | Merge PR #1131: Clean-up xml protocol doc | Maxime Dénès | |
| 2017-10-06 | Merge PR #1129: 8.7+beta2 CHANGES | Maxime Dénès | |
| 2017-10-06 | Merge PR #1123: [ci] Remove deploy to GitHub of OS X package. | Maxime Dénès | |
| 2017-10-06 | TimeFileMaker.py: Allow trailing spaces | Jason Gross | |
| This allows the timing aggregation scripts to handle logs from Travis, which, for some reason, seems to insert trailing spaces. | |||
| 2017-10-06 | Extract changes to the XML protocol from its doc | Théo Zimmermann | |
| 2017-10-06 | Make the XML protocol doc more version-independent | Théo Zimmermann | |
| 2017-10-06 | Fix copyright info in reference manual. | Théo Zimmermann | |
| Also simplifies the way it is presented (no need to be overly precise). | |||
| 2017-10-06 | 8.7+beta2 CHANGES | Thé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-05 | romega: takes advantage of context variables with body | Pierre 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-05 | Omega 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-05 | Merge PR #1069: Improve support for -w options | Maxime Dénès | |
| 2017-10-05 | Merge PR #1081: Mini fix at improving the cannot unify error message | Maxime Dénès | |
| 2017-10-05 | Fix typo in INSTALL | Maxime Dénès | |
| 2017-10-05 | Merge 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-05 | Merge PR #1093: [doc] Update INSTALL to match reality. | Maxime Dénès | |
| 2017-10-05 | Merge PR #1107: Add coqwc tests to test suite | Maxime Dénès | |
| 2017-10-05 | GitLab CI: make all_stdlib.v in build job | Gaëtan Gilbert | |
| 2017-10-05 | Merge PR #1106: Fix beautifier | Maxime Dénès | |
| 2017-10-05 | Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵ | Maxime Dénès | |
| BZ#5757) | |||
| 2017-10-05 | Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵ | Maxime Dénès | |
| cleared context. | |||
| 2017-10-05 | Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵ | Maxime Dénès | |
| coq_makefile are in sync (supersed #1039)… | |||
| 2017-10-05 | Merge PR #1112: Fix GeoCoq CI and remove it from allowed failures | Maxime Dénès | |
| 2017-10-05 | Extraction: reduce eta-redexes whose cores are atomic (solves indirectly ↵ | Pierre Letouzey | |
| BZ#4852) This code simplification isn't that important, but it can trigger further simplifications elsewhere, see for instance BZ#4852. NB: normally, the extraction favors eta-expanded forms, since that's the usual way to avoid issues about '_a type variables that cannot be generalized. But the atomic eta-reductions done here shouldn't be problematic (no applications put outside of functions). | |||
| 2017-10-05 | Shorten the .gitattributes file. | Théo Zimmermann | |
| .dir-locals.el can be useful for users of the tarballs as well, and TODO doesn't exist anymore. | |||
| 2017-10-05 | [pp] Minor optimization in `Pp.t` construction and gluing. | Emilio Jesus Gallego Arias | |
| The typical Coq `Pp.t` document contains a lot of "gluing" which produces efficient structures but it is quite painful in serialization. We optimize a common document building case so we don't create as much glue nodes as with the "naive" strategy, and without incurring in the large performance cost full flattening would produce. This is a temporal fixup, see #505 for more context on the discussion and medium-term plans. | |||
| 2017-10-05 | [ci] Remove deploy to GitHub of OS X package. | Théo Zimmermann | |
| This is inconvenient because it can only be tested on tags and it didn't work for V8.7+beta1. | |||
| 2017-10-05 | Fixing BZ#5769 (variable of type "_something" was named after invalid "_"). | Hugo Herbelin | |
| 2017-10-05 | Distinguishing pseudo-letters out of the set of unicode letters. | Hugo Herbelin | |
| This includes _ and insecable space which can be used in idents and this allows more precise heuristics. | |||
| 2017-10-05 | Fixing typos in comments of unicode.ml. | Hugo Herbelin | |
| 2017-10-05 | Fixing #5765 (an anomaly with 'pat in parameters of inductive definition). | Hugo Herbelin | |
| 2017-10-05 | Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.). | Hugo Herbelin | |
| This allows e.g. the following to work: Reserved Notation "* a" (at level 70). Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m). We seize this opportunity to make main calls to Metasyntax to depend on an arbitrary env rather than on Global.env. Incidentally, this fixes a little coqdoc bug in classifying the inductive type referred to in the "where" clause. | |||
| 2017-10-04 | Merge PR #1006: fix: ssrmatching and primitive projections | Maxime Dénès | |
| 2017-10-04 | Merge PR #1078: Report missing arguments in error message | Maxime Dénès | |
| 2017-10-04 | Extraction : minor support stuff for the new Extraction Compute plugin | Pierre Letouzey | |
| See https://github.com/letouzey/extraction-compute for more details | |||
| 2017-10-04 | Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677] | Maxime Dénès | |
| 2017-10-04 | [ci] Remove temporary bignums overlay. | Théo Zimmermann | |
| 2017-10-04 | Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial). | Maxime Dénès | |
| 2017-10-03 | add coqwc tests | Paul Steckler | |
| 2017-10-03 | autolink to Github PRs from Bugzilla | Paul Steckler | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |