aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-08-06Merge PR #8189: Some trivial fixes to the custom entry documentation.Emilio Jesus Gallego Arias
2018-08-06Merge PR #8073: Use GitHub as the location for OCaml sources.Michael Soegtrop
2018-08-04Merge PR #8142: Improved the grammar and spelling of chapter 'Syntax ↵Théo Zimmermann
extensions and interpretation scopes' of the Reference Manual.
2018-08-04Improved the grammar and spelling of chapter 'Syntax extensions and ↵Zeimer
interpretation scopes' of the Reference Manual.
2018-08-04Merge PR #8216: Fix docs on arguments to setoid_replaceThéo Zimmermann
2018-08-03Fix docs on arguments to setoid_replace. Fixes #8213Langston Barrett
2018-08-02Merge PR #8143: Improved grammar and spelling in chapters 'Proof Schemes' ↵Théo Zimmermann
and 'The Coq commands' of the Reference Manual.
2018-08-02Merge PR #8145: Improved grammar and spelling in chapter 'Extended pattern ↵Théo Zimmermann
matching' of the Reference Manual.
2018-08-02Merge PR #8144: Improved grammar and spelling for chapters 'Utilities' and ↵Théo Zimmermann
'CoqIDE' of the Reference Manual.
2018-08-02Merge PR #8176: Improved grammar and spelling in chapters 'Type Classes', ↵Théo Zimmermann
'Omega' and 'Micromega' of the Reference Manual.
2018-08-02Merge PR #8185: Improved grammar and spelling in the remaining chapters of ↵Théo Zimmermann
the Reference Manual.
2018-08-01Added a tactic index entry for nsatz, reformatted commands in chapter ↵Zeimer
'Generalized Rewriting' and renamed the chapter Nsatz from _nsatz to _nsatz_chapter.
2018-08-01Improved grammar and spelling in the remaining chapters of the Reference Manual.Zeimer
2018-08-01Improved grammar and spelling in chapter 'Extended pattern matching' of the ↵Zeimer
Reference Manual.
2018-08-01Improved grammar and spelling in chapters 'Proof Schemes' and 'The Coq ↵Zeimer
commands' of the Reference Manual.
2018-08-01Improved grammar and spelling in chapters 'Type Classes', 'Omega' and ↵Zeimer
'Micromega' of the Reference Manual.
2018-08-01Merge PR #8169: NArith: add sized N2BvHugo Herbelin
2018-08-01Improved grammar and spelling for chapters 'Utilities' and 'CoqIDE' of the ↵Zeimer
Reference Manual.
2018-08-01Merge PR #8151: Vector: expose ++ to userHugo Herbelin
2018-08-01Merge PR #8182: Handle diffs better for the "Undo" command.Enrico Tassi
2018-08-01Merge PR #8192: Fix typos and typesetting of doc on ProgramThéo Zimmermann
2018-08-01Merge PR #8184: Improved grammar and spelling in chapters 'Extraction', ↵Théo Zimmermann
'Program' and 'ring and field' chapters of the Reference Manual.
2018-08-01Merge PR #8191: [sphinx] Use arguments of '.. example::' directive as a titleThéo Zimmermann
2018-08-01Merge PR #8195: Fix doc for no associativityThéo Zimmermann
2018-07-31Camlp{4 => 5}Jason Gross
2018-07-31Code to handle "Back" command for diffs.Jim Fehrle
2018-07-31Fix doc for no associativityJason 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-30Fix typos and typesetting of doc on ProgramLysxia
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClé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-30Merge PR #8113: Make universe object DisposePierre-Marie Pédrot
2018-07-30CHANGES: unify formatYishuai Li
2018-07-30CHANGES: note potential incompatibilities with ++Yishuai Li
2018-07-30Vector: expose ++ to userYishuai Li
2018-07-30Merge PR #8137: Fix 8132. Print the content of body, not its type.Hugo Herbelin
2018-07-30Some trivial fixes to the custom entry documentation.Théo Zimmermann
2018-07-30Merge PR #8115: Support for custom entries in notations (take 2, feature part)Emilio Jesus Gallego Arias
2018-07-29Fix 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-29Improved grammar and spelling in chapters 'Extraction', 'Program' and 'ring ↵Zeimer
and field' chapters of the Reference Manual.
2018-07-29Miscellaneous uniformization of typography in chapter syntax extensions.Hugo Herbelin
2018-07-29Documenting custom entries in the reference manual + CHANGES.Hugo Herbelin
2018-07-29Store marshallable data in the custom entry summary.Pierre-Marie Pédrot
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
Also prevents to use an entry name already defined.
2018-07-29Do not treat curly brackets specially in custom entries.Hugo Herbelin
2018-07-29Classify "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-29Renaming ETName and ETReference so as to fit the user-visible terminology.Hugo Herbelin
ETName -> ETIdent ETReference -> ETGlobal
2018-07-29Adding 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-29A 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-29Synchronizing "grammars by name" with backtrack (custom entries shall be ↵Hugo Herbelin
added incrementally).
2018-07-28Merge PR #8077: Fix #7291: unify tactic should have more descriptive error ↵Hugo Herbelin
messages.
2018-07-28Merge PR #8160: Improved chapters 'Implicit Coercions' and 'Canonical ↵Théo Zimmermann
Structures' of the Reference Manual.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 12:42:57 +0000