| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-20 | [test-suite] Add tests for goal printing. | Emilio Jesus Gallego Arias | |
| - https://coq.inria.fr/bugs/show_bug.cgi?id=5529 - https://coq.inria.fr/bugs/show_bug.cgi?id=5537 See also PR #640 | |||
| 2017-05-20 | Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.el | Maxime Dénès | |
| 2017-05-20 | Merge PR#649: Fix a typo | Maxime Dénès | |
| 2017-05-20 | Merge PR#651: Re-adding explicit dependency of misc universe test into ↵ | Maxime Dénès | |
| all_stdlib.v. | |||
| 2017-05-20 | Merge PR#640: [toplevel] Restore 8.6 goal printing behavior. | Maxime Dénès | |
| 2017-05-19 | Re-adding explicit dependency of misc universe test into all_stdlib.v. | Hugo Herbelin | |
| Was working when calling test-suite from main Makefile but not when calling directly from the test-suite Makefile. The dependency was mistakenly dropped in 98a927aef. | |||
| 2017-05-18 | Fix a typo | Jason Gross | |
| 2017-05-18 | Add .dir-locals.el to plugins | Jason Gross | |
| As requested in https://github.com/coq/coq/pull/386#issuecomment-302358542 | |||
| 2017-05-17 | Merge PR#633: An extension of EXTEND and notations to make standard parsing ↵ | Maxime Dénès | |
| tricks available to users | |||
| 2017-05-17 | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès | |
| 2017-05-17 | Merge PR#607: Make congruence reuse discriminate instead of rolling its own. | Maxime Dénès | |
| 2017-05-17 | [toplevel] Restore 8.6 goal printing behavior. | Emilio Jesus Gallego Arias | |
| When porting the toplevel to the STM, the logic for goal printing was simplified too much under optimistic assumptions. The idea was not to rely on the `vernac_classifier` which is an internal and complicated beast. However, it seems there are many cases to consider other than `is_query`, so at the risk of reimplementing the classifier we revert to the old approach of using the full classification. This gives maximum 8.6 compatibility, with the pitfall of having to call the classifier. Indeed, due to the dynamic nature of the "undo classifier", we cannot call it after `Stm.add`, as the document tree will be not the right one, making the classification of undo commands incorrect (actually raising an error "Cannot undo"). | |||
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-05-17 | Merge PR#620: Reorganization of the layout for miscellaneous tests | Maxime Dénès | |
| 2017-05-17 | Merge PR#614: Improve Travis | Maxime Dénès | |
| 2017-05-17 | Travis: add -warn-error targets (standard and 4.04.1 ocaml) | Gaetan Gilbert | |
| 2017-05-17 | Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanup | Maxime Dénès | |
| 2017-05-17 | Travis: deduplicate package list for coqide+documentation targets | Gaetan Gilbert | |
| 2017-05-17 | Travis: do not run the tests if building Coq fails | Gaetan Gilbert | |
| 2017-05-17 | Merge PR#635: Fixing #5522 (anomaly with free vars of pat) | Maxime Dénès | |
| 2017-05-17 | Merge PR#636: Miscellaneous typos, dead code, etc. | Maxime Dénès | |
| 2017-05-17 | Merge PR#639: Stop using auto with * in two proofs. | Maxime Dénès | |
| 2017-05-16 | Stop using auto with * in two proofs. | Théo Zimmermann | |
| auto with * is an overkill for people who do not care to understand what they really need. In these two cases, one lemma which was available in the typeclass_instances hint db. | |||
| 2017-05-16 | Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND. | Hugo Herbelin | |
| 2017-05-16 | Adding support for using grammar entries returning no value in EXTEND. | Hugo Herbelin | |
| 2017-05-16 | Simplified compaction criterion + tests. | Pierre Courtieu | |
| 2017-05-16 | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters). | Hugo Herbelin | |
| We seized this opportunity to factorize the code for interning `pat with more general pre-existing code. More precisely: There was already a function to compute the free variables of a pattern. Commit c6d9d4fb rewrote an approximation of it and #5222 hits cases non-treated by this function. We remove the partially-defined redundant code and use instead the existing code since intern_cases_pattern, already called, was already doing this computation. (In doing so, we discover a bug in merging names in the presence of nested "as" clauses, which we fix in previous commit. Additionally, intern_local_pattern was misleadingly overkill to simply mean a folding on Id.Set.add and we avoid the detour. | |||
| 2017-05-16 | Fixing a bug with nested "as" clauses in "match". | Hugo Herbelin | |
| 2017-05-16 | Merge PR#624: Switch bedrock to mit-plv base | Maxime Dénès | |
| 2017-05-16 | Merge PR#626: Add documentation for Set Ltac Batch Debug | Maxime Dénès | |
| 2017-05-16 | Merge PR#629: A couple of simple updates for Travis | Maxime Dénès | |
| 2017-05-15 | Dead code in coqdep. | Hugo Herbelin | |
| Was introduced in 5268efdef, reverted then readded in 1be9c4d. | |||
| 2017-05-15 | [interp] Rework check for casts inside patterns. | Emilio Jesus Gallego Arias | |
| 1969e10f25df0c913600099b7b98ea273a064017 introduced a check so a cast in a pattern is not a fatal error. We move this check to the internalization function, which is the logical place to raise it, removing a bit boilerplate code. | |||
| 2017-05-15 | [interp] [ast] Make raw_cases_pattern_expr private. | Emilio Jesus Gallego Arias | |
| The type `raw_cases_pattern_expr` is used only in the interpretation of notation patterns. Indeed, this should be a private type thus we make it local to `Constrintern`; it makes no sense to expose it in the public AST. The patch is routine, except for the case used to interpret primitives in patterns. We now return a `glob_constr` representing the raw pattern, instead of the private raw pattern type. This could be further refactored but have opted to be conservative here. This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754 , see the commentaries there for more information about `raw_cases_pattern_expr`. | |||
| 2017-05-15 | Typo in comments of constrintern. | Hugo Herbelin | |
| 2017-05-14 | Removing a line warned unused. | Hugo Herbelin | |
| 2017-05-14 | Removing a variable warned unused. | Hugo Herbelin | |
| 2017-05-13 | [travis] Update OCaml to 4.04.1 | Emilio Jesus Gallego Arias | |
| 2017-05-13 | [travis] Move VST to required suite. | Emilio Jesus Gallego Arias | |
| 2017-05-13 | Uniformity of style for selecting plural or not; spacing for comma. | Hugo Herbelin | |
| 2017-05-13 | Typo in a comment of plugin Quote. | Hugo Herbelin | |
| 2017-05-13 | Aligning on standard layout of CHANGES. | Hugo Herbelin | |
| 2017-05-11 | Add documentation for Set Ltac Batch Debug | Jason Gross | |
| 2017-05-11 | Documenting Printing Compact Contexts + CHANGES | Pierre Courtieu | |
| 2017-05-11 | Merge PR#594: An example showing the benefit of Econstr | Maxime Dénès | |
| 2017-05-11 | Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 ↵ | Maxime Dénès | |
| and 8.5/8.6 "refine" | |||
| 2017-05-11 | Merge PR#572: Replacing costly merges in UGraph. | Maxime Dénès | |
| 2017-05-11 | Remove an unused open introduced by the previous commit. | Maxime Dénès | |
| 2017-05-11 | Merge PR#201: Transparent abstract | Maxime Dénès | |
| 2017-05-10 | Switch bedrock to mit-plv base | Jason Gross | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |