aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2016-03-04Uniformizing the parsing of argument scopes in Ltac.Pierre-Marie Pédrot
2016-02-29Moving the "move" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "exists" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "symmetry" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "generalize dependent" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clearbody" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clear" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "cofix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "fix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-24Removing the METAIDENT token, as it is not used anymore.Pierre-Marie Pédrot
2016-02-24Removing the MetaIdArg entry of tactic expressions.Pierre-Marie Pédrot
2016-02-02Removing a source of type-unsafeness in Pcoq.Pierre-Marie Pédrot
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2016-01-17Simplification and type-safety of Pcoq thanks to GADTs in Genarg.Pierre-Marie Pédrot
2016-01-17Temporary commit getting rid of Obj.magic unsafety for Genarg.Pierre-Marie Pédrot
2016-01-17Removing dynamic entries from Pcoq.Pierre-Marie Pédrot
2016-01-17ML extensions use untyped representation of user entries.Pierre-Marie Pédrot
2016-01-16Separating the parsing of user-defined entries from their intepretation.Pierre-Marie Pédrot
2016-01-16Less type-unsafety in Pcoq.Pierre-Marie Pédrot
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-14Continuing 003fe3d5e on parsing positions.Hugo Herbelin
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-02Remove some useless type declarations.Guillaume Melquiond
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2016-01-02Separation of concern in TacAlias API.Pierre-Marie Pédrot
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
2015-12-28Removing unused parsing entries.Pierre-Marie Pédrot
2015-12-28Removing the special status of open_constr generic argument.Pierre-Marie Pédrot
2015-12-25Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlHugo Herbelin
2015-12-25Fixing non exhaustive pattern-matching in 003fe3d5e60b.Hugo Herbelin
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-23Partial backtrack on commit 20641795624.Pierre-Marie Pédrot
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-18CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionMatej Kosik
2015-12-18ALPHA-CONVERSION: in "parsing/g_vernac.ml4" fileMatej Kosik
2015-12-18CLEANUP: Vernacexpr.vernac_exprMatej Kosik
2015-12-15Adding a token "index" representing positions (1st, 2nd, etc.).Hugo Herbelin
2015-12-15Tactics: Generalizing the use of the experimental clearing modifier toHugo Herbelin
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Improving syntax of pat/constr introduction pattern so thatHugo Herbelin
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:33:46 +0000