aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Gravatar Hugo Herbelin2015-12-05
* Improving syntax of pat/constr introduction pattern so thatGravatar Hugo Herbelin2015-12-02
* Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
* Fixing the "parsing rules with idents later declared as keywords" problem.Gravatar Hugo Herbelin2015-11-26
* Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* Manually expand red_tactic so that notations do not break reduction tactics. ...Gravatar Guillaume Melquiond2015-10-30
* Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)Gravatar Guillaume Melquiond2015-10-29
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Allowing empty bound universe variables.Gravatar Pierre-Marie Pédrot2015-10-08
* Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* Record fields accept an optional final semicolon separator.Gravatar Pierre-Marie Pédrot2015-10-07
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Hacking parser so as to support both [> ... ] and [id].Gravatar Hugo Herbelin2015-09-08
* Removing the G_xml module again.Gravatar Pierre-Marie Pédrot2015-07-22
* Notation: use same level for "@" in constr: and pattern: (Close: #4272)Gravatar Enrico Tassi2015-07-01
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Granting, undocumentedly, parsing of "Conjectures" as a synonym ofGravatar Hugo Herbelin2015-06-16
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Inlining "fun" and "forall" tokens in parser, so that alternative notations forGravatar Hugo Herbelin2015-04-20
* grammar: export constr_evalGravatar Enrico Tassi2015-03-30
* grammar: export hypidentGravatar Enrico Tassi2015-03-30
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
* Qed export -> Qed exportingGravatar Enrico Tassi2015-03-22
* Fixed 3233 (fresh does not work with a qualid).Gravatar Pierre Courtieu2015-02-23
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Fixing #3982 (conflict with max notation for universes).Gravatar Hugo Herbelin2015-02-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* A global [gfail] tactic which works like [fail] except that it fails even if ...Gravatar Arnaud Spiwack2014-12-23
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
* Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)Gravatar Hugo Herbelin2014-11-06
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* Reorganization of the test for generic selection of occurrences inGravatar Hugo Herbelin2014-10-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 11:05:23 +0000