index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
Commit message (
Expand
)
Author
Age
*
Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].
Pierre-Marie Pédrot
2016-03-04
*
Exchanging roles of tactic_arg and tactic_top_or_arg entries.
Pierre-Marie Pédrot
2016-03-04
*
Removing the UConstr entry of the tactic_arg AST.
Pierre-Marie Pédrot
2016-03-04
*
Making parentheses mandatory in tactic scopes.
Pierre-Marie Pédrot
2016-03-04
*
Uniformizing the parsing of argument scopes in Ltac.
Pierre-Marie Pédrot
2016-03-04
*
Moving the "move" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
Moving the "exists" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
Moving the "symmetry" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
Moving the "generalize dependent" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
Moving the "clearbody" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
Moving the "clear" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
Moving the "cofix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
Moving the "fix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
Removing the METAIDENT token, as it is not used anymore.
Pierre-Marie Pédrot
2016-02-24
*
Removing the MetaIdArg entry of tactic expressions.
Pierre-Marie Pédrot
2016-02-24
*
Removing a source of type-unsafeness in Pcoq.
Pierre-Marie Pédrot
2016-02-02
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
*
Implement support for universe binder lists in Instance and Program Fixpoint/...
Matthieu Sozeau
2016-01-23
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
|
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
Hugo Herbelin
2016-01-21
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Simplification and type-safety of Pcoq thanks to GADTs in Genarg.
Pierre-Marie Pédrot
2016-01-17
*
|
Temporary commit getting rid of Obj.magic unsafety for Genarg.
Pierre-Marie Pédrot
2016-01-17
*
|
Removing dynamic entries from Pcoq.
Pierre-Marie Pédrot
2016-01-17
*
|
ML extensions use untyped representation of user entries.
Pierre-Marie Pédrot
2016-01-17
*
|
Separating the parsing of user-defined entries from their intepretation.
Pierre-Marie Pédrot
2016-01-16
*
|
Less type-unsafety in Pcoq.
Pierre-Marie Pédrot
2016-01-16
|
*
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
|
Removing constr generic argument.
Pierre-Marie Pédrot
2016-01-14
*
|
Continuing 003fe3d5e on parsing positions.
Hugo Herbelin
2016-01-14
*
|
CLEANUP: removing unused field
Matej Kosik
2016-01-11
*
|
Remove some useless type declarations.
Guillaume Melquiond
2016-01-02
*
|
Simplification of grammar_prod_item type.
Pierre-Marie Pédrot
2016-01-02
*
|
Separation of concern in TacAlias API.
Pierre-Marie Pédrot
2016-01-02
*
|
External tactics and notations now accept any tactic argument.
Pierre-Marie Pédrot
2015-12-30
*
|
Removing unused parsing entries.
Pierre-Marie Pédrot
2015-12-28
*
|
Removing the special status of open_constr generic argument.
Pierre-Marie Pédrot
2015-12-28
*
|
Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.ml
Hugo Herbelin
2015-12-25
*
|
Fixing non exhaustive pattern-matching in 003fe3d5e60b.
Hugo Herbelin
2015-12-25
*
|
Removing auto from the tactic AST.
Pierre-Marie Pédrot
2015-12-24
*
|
Partial backtrack on commit 20641795624.
Pierre-Marie Pédrot
2015-12-23
*
|
CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified
Matej Kosik
2015-12-18
*
|
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
Matej Kosik
2015-12-18
*
|
ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file
Matej Kosik
2015-12-18
*
|
CLEANUP: Vernacexpr.vernac_expr
Matej Kosik
2015-12-18
*
|
Adding a token "index" representing positions (1st, 2nd, etc.).
Hugo Herbelin
2015-12-15
*
|
Tactics: Generalizing the use of the experimental clearing modifier to
Hugo Herbelin
2015-12-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-11
|
\
|
|
*
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Hugo Herbelin
2015-12-10
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
[next]