aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2015-09-25Add (temporary) syntax for assuming guardedness in (co-)fixed points.Arnaud Spiwack
2015-09-25Add `Guarded` to the assumption tokens.Arnaud Spiwack
2015-09-25Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...Arnaud Spiwack
2015-06-24Add syntax entry to assume strict positivity of an inductive type.Arnaud Spiwack
2015-06-24Add corresponding field in `VernacInductive`.Arnaud Spiwack
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
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-12Fixing #3982 (conflict with max notation for universes).Hugo Herbelin
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-23A global [gfail] tactic which works like [fail] except that it fails even if ...Arnaud Spiwack
2014-12-23Fix compilation error in some configurations.Arnaud Spiwack
2014-12-19Add a backtracking version of Ltac's [match].Arnaud Spiwack
2014-12-19Better doc and a few fixes for Proof using.Enrico Tassi
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-15About now accepts hypothesis names and goal selector.Pierre Courtieu
2014-12-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-12-12Searchxxx now search also the hypothesis and support goal selector.Pierre Courtieu
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
2014-11-06Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)Hugo Herbelin
2014-11-02Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Hugo Herbelin
2014-11-01Add [Info] command.Arnaud Spiwack
2014-10-31Reorganization of the test for generic selection of occurrences inHugo Herbelin
2014-10-27Dead codeHugo Herbelin
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-13Emit a warning for void Arguments statement (Close 3713)Enrico Tassi
2014-10-13Parsing of "?[" as two tokens (makes ssr compile).Enrico Tassi
2014-10-07Fixing #3687 (inconsistent lexer state after a bullet).Hugo Herbelin
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 07:10:00 +0000