aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Simplification and type-safety of Pcoq thanks to GADTs in Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | Temporary commit getting rid of Obj.magic unsafety for Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | Removing dynamic entries from Pcoq.Gravatar Pierre-Marie Pédrot2016-01-17
* | ML extensions use untyped representation of user entries.Gravatar Pierre-Marie Pédrot2016-01-17
* | Separating the parsing of user-defined entries from their intepretation.Gravatar Pierre-Marie Pédrot2016-01-16
* | Less type-unsafety in Pcoq.Gravatar Pierre-Marie Pédrot2016-01-16
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
* | Continuing 003fe3d5e on parsing positions.Gravatar Hugo Herbelin2016-01-14
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | Remove some useless type declarations.Gravatar Guillaume Melquiond2016-01-02
* | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* | Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* | Removing unused parsing entries.Gravatar Pierre-Marie Pédrot2015-12-28
* | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlGravatar Hugo Herbelin2015-12-25
* | Fixing non exhaustive pattern-matching in 003fe3d5e60b.Gravatar Hugo Herbelin2015-12-25
* | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* | Partial backtrack on commit 20641795624.Gravatar Pierre-Marie Pédrot2015-12-23
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
* | ALPHA-CONVERSION: in "parsing/g_vernac.ml4" fileGravatar Matej Kosik2015-12-18
* | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
* | Adding a token "index" representing positions (1st, 2nd, etc.).Gravatar Hugo Herbelin2015-12-15
* | Tactics: Generalizing the use of the experimental clearing modifier toGravatar Hugo Herbelin2015-12-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Gravatar Hugo Herbelin2015-12-05
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Fixing the "parsing rules with idents later declared as keywords" problem.Gravatar Hugo Herbelin2015-11-26
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
|\|
| * 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
* | Fixing the return type of the Atoken symbol.Gravatar Pierre-Marie Pédrot2015-10-28
* | Removing unused code in Pcoq.Gravatar Pierre-Marie Pédrot2015-10-27
* | Type-safe Egramml.grammar_prod_item.Gravatar Pierre-Marie Pédrot2015-10-27
* | Finer type for Pcoq.interp_entry_name.Gravatar Pierre-Marie Pédrot2015-10-27
* | Getting rid of most uses of unsafe_grammar_extend.Gravatar Pierre-Marie Pédrot2015-10-27
* | Type-safe Egramml.make_rule.Gravatar Pierre-Marie Pédrot2015-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 18:43:40 +0000