aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2015-10-28Fixing the return type of the Atoken symbol.Pierre-Marie Pédrot
2015-10-27Removing unused code in Pcoq.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-27Finer type for Pcoq.interp_entry_name.Pierre-Marie Pédrot
2015-10-27Getting rid of most uses of unsafe_grammar_extend.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.make_rule.Pierre-Marie Pédrot
2015-10-27Indexing existentially quantified entries returned by interp_entry_name.Pierre-Marie Pédrot
2015-10-27Type-safe grammar extensions.Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
2015-10-25Getting rid of the Atactic entry.Pierre-Marie Pédrot
2015-10-25Getting rid of the Agram entry.Pierre-Marie Pédrot
2015-10-21Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Pierre-Marie Pédrot
2015-10-21Turn Pcoq into a regular ML file.Pierre-Marie Pédrot
2015-10-21Expanding the grammar extensions of Pcoq.Pierre-Marie Pédrot
2015-10-21Removing the dependencies of Pcoq in IFDEF macros.Pierre-Marie Pédrot
2015-10-21Expliciting some uses of Compat module.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08Allowing empty bound universe variables.Pierre-Marie Pédrot
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-10-07Record fields accept an optional final semicolon separator.Pierre-Marie Pédrot
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-09-09Merge remote-tracking branch 'origin/v8.5' into trunkHugo Herbelin
2015-09-08Hacking parser so as to support both [> ... ] and [id].Hugo Herbelin
2015-07-27Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-22Removing the G_xml module again.Pierre-Marie Pédrot
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-07-01Notation: use same level for "@" in constr: and pattern: (Close: #4272)Enrico Tassi
2015-06-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-16Granting, undocumentedly, parsing of "Conjectures" as a synonym ofHugo Herbelin
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-20Inlining "fun" and "forall" tokens in parser, so that alternative notations forHugo Herbelin
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-30grammar: export constr_evalEnrico Tassi
2015-03-30grammar: export hypidentEnrico Tassi
2015-03-27Putting the From parameter of the Require command into the AST.Pierre-Marie Pédrot
2015-03-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-22Qed export -> Qed exportingEnrico Tassi
2015-02-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-23Fixed 3233 (fresh does not work with a qualid).Pierre Courtieu
2015-02-15Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 17:38:49 +0000