| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-31 | Code to handle "Back" command for diffs. | Jim Fehrle | |
| 2018-07-31 | Fix doc for no associativity | Jason Gross | |
| no associative -> no associativity Also remove some 'a's and 'the's and make a note that this is for parsing (There is a difference between left associativity and no associativity for printing) | |||
| 2018-07-30 | Fix typos and typesetting of doc on Program | Lysxia | |
| 2018-07-30 | [sphinx] Use arguments of '.. example::' directive as a title | Clément Pit-Claudel | |
| Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines. | |||
| 2018-07-30 | Merge PR #8113: Make universe object Dispose | Pierre-Marie Pédrot | |
| 2018-07-30 | CHANGES: unify format | Yishuai Li | |
| 2018-07-30 | CHANGES: note potential incompatibilities with ++ | Yishuai Li | |
| 2018-07-30 | Vector: expose ++ to user | Yishuai Li | |
| 2018-07-30 | Merge PR #8137: Fix 8132. Print the content of body, not its type. | Hugo Herbelin | |
| 2018-07-30 | Some trivial fixes to the custom entry documentation. | Théo Zimmermann | |
| 2018-07-30 | Merge PR #8115: Support for custom entries in notations (take 2, feature part) | Emilio Jesus Gallego Arias | |
| 2018-07-29 | Fix issue 8132. Print the content of body as in Printer.pr_compacted_decl, | Jim Fehrle | |
| not the type of body. Also update CHANGES to reflect that the argument for Set Diffs is a string. | |||
| 2018-07-29 | Improved grammar and spelling in chapters 'Extraction', 'Program' and 'ring ↵ | Zeimer | |
| and field' chapters of the Reference Manual. | |||
| 2018-07-29 | Miscellaneous uniformization of typography in chapter syntax extensions. | Hugo Herbelin | |
| 2018-07-29 | Documenting custom entries in the reference manual + CHANGES. | Hugo Herbelin | |
| 2018-07-29 | Store marshallable data in the custom entry summary. | Pierre-Marie Pédrot | |
| 2018-07-29 | Supporting locality flag for custom entries + compatibility with modules. | Hugo Herbelin | |
| Also prevents to use an entry name already defined. | |||
| 2018-07-29 | Do not treat curly brackets specially in custom entries. | Hugo Herbelin | |
| 2018-07-29 | Classify "Declare Custom" as VtNow for the stm. | Hugo Herbelin | |
| When parsing of a document shall be possible independently of interpretation, this shall however be indicated as shall be interpreted now so that the notation commands coming next work. | |||
| 2018-07-29 | Renaming ETName and ETReference so as to fit the user-visible terminology. | Hugo Herbelin | |
| ETName -> ETIdent ETReference -> ETGlobal | |||
| 2018-07-29 | Adding support for custom entries in notations. | Hugo Herbelin | |
| - New command "Declare Custom Entry bar". - Entries can have levels. - Printing is done using a notion of coercion between grammar entries. This typically corresponds to rules of the form 'Notation "[ x ]" := x (x custom myconstr).' but also 'Notation "{ x }" := x (in custom myconstr, x constr).'. - Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).' are natively recognized. - Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).' are natively recognized. Incidentally merging ETConstr and ETConstrAsBinder. Noticed in passing that parsing binder as custom was not done as in constr. Probably some fine-tuning still to do (priority of notations, interactions between scopes and entries, ...). To be tested live further. | |||
| 2018-07-29 | A test on the different ways to indicate the levels of a rule. | Hugo Herbelin | |
| This is in preparation of changes in level_eq, to check that the semantics is preserved. | |||
| 2018-07-29 | Synchronizing "grammars by name" with backtrack (custom entries shall be ↵ | Hugo Herbelin | |
| added incrementally). | |||
| 2018-07-28 | Merge PR #8077: Fix #7291: unify tactic should have more descriptive error ↵ | Hugo Herbelin | |
| messages. | |||
| 2018-07-28 | Merge PR #8160: Improved chapters 'Implicit Coercions' and 'Canonical ↵ | Théo Zimmermann | |
| Structures' of the Reference Manual. | |||
| 2018-07-28 | Merge PR #8148: Doc: preliminary work before #7291 which add an "Unable to ↵ | Théo Zimmermann | |
| unify" message | |||
| 2018-07-27 | Merge PR #8174: [ci] Remove CircleCI setup. | Gaëtan Gilbert | |
| 2018-07-27 | Merge PR #8173: Missing backslash in a documentation file. | Théo Zimmermann | |
| 2018-07-27 | [ci] Remove CircleCI setup. | Emilio Jesus Gallego Arias | |
| GitLab setup is quite stable these days thanks to the work of many people and `coqbot`. We decided to keep CircleCI support for a while as a safeguard in case something happened in the migration to GitLab, but these days we are just wasting resources to them and to us. As I'm afraid CircleCI won't scale for us, the time to remove it has arrived. Still, CircleCI had some awesome functionality that GitLab's CI doesn't offer yet, see the links at: https://github.com/coq/coq/issues/6919#issuecomment-395885573 - https://gitlab.com/gitlab-org/gitlab-ce/issues/29347 - https://gitlab.com/gitlab-org/gitlab-ce/issues/35222 - https://gitlab.com/gitlab-org/gitlab-ce/issues/41947 - https://gitlab.com/gitlab-org/gitlab-ce/issues/47063 | |||
| 2018-07-27 | Missing backslash in the documentation file. | Martin Bodin | |
| 2018-07-27 | Merge PR #8164: Add information to option type errors | Enrico Tassi | |
| 2018-07-27 | Merge PR #8166: Fix Search query in CoqIDE. | Enrico Tassi | |
| 2018-07-27 | Merge PR #8103: Coercions cleanup: use GlobRef.t instead of constr | Enrico Tassi | |
| 2018-07-27 | Merge PR #8141: Diff option in CoqIDE | Enrico Tassi | |
| 2018-07-26 | [sphinx] Do name cleanup in handle_signature | Clément Pit-Claudel | |
| 2018-07-26 | NArith: add sized N2Bv | Yishuai Li | |
| 2018-07-26 | Merge PR #8101: Remove ClosedModule and ClosedSection from libstack | Enrico Tassi | |
| 2018-07-26 | Fix Search query in CoqIDE. | Pierre-Marie Pédrot | |
| For some reason the code was just doing random stuff that did not make sense. | |||
| 2018-07-26 | Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the ↵ | Zeimer | |
| Reference Manual. | |||
| 2018-07-26 | Add information to option type errors | Tej Chajed | |
| Print the expected and actual types for the option value (which is one of bool, int, or string). | |||
| 2018-07-26 | Replace iter + ref by fold_left | Maxime Dénès | |
| 2018-07-26 | restore reduction of coercion to eventually expose a constructor | Enrico Tassi | |
| 2018-07-26 | Coercions cleanup: use GlobRef.t instead of constr | Maxime Dénès | |
| 2018-07-26 | Don't use an object for polymorphic section universes | Gaëtan Gilbert | |
| 2018-07-26 | Universe object is Dispose | Gaëtan Gilbert | |
| 2018-07-26 | Merge PR #8100: Use just one object declaration for all global universe ↵ | Pierre-Marie Pédrot | |
| additions | |||
| 2018-07-26 | Fix #8121: anomalies in native_compute with let and evars. | Pierre-Marie Pédrot | |
| Même causes, mêmes effets, similar fix to #8119: - Do not pass let-bound arguments to evars. We seize the opportunity to remove the useless type information for Aevar. Special fixes to native compilation: - Evars are not handled correctly when iterating over lambda terms. - Names.id_of_string is gone. - Evar instances are not reified in the right order. | |||
| 2018-07-26 | Adding an overlay for Mtac2. | Pierre-Marie Pédrot | |
| 2018-07-26 | Turn the kernel reduction sharing flag into an argument passed in the cache. | Pierre-Marie Pédrot | |
| We move the global declaration of that argument to the environment, and reuse the Global module to handle this flag. Note that the checker was not using this flag before this patch, and still doesn't use it. This should probably be fixed in a later patch. | |||
| 2018-07-26 | Merge PR #8050: Cleanup VERNAC EXTEND | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |