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
*
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
|
\
|
|
*
Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)
Hugo Herbelin
2015-12-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
|
|
*
Improving syntax of pat/constr introduction pattern so that
Hugo Herbelin
2015-12-02
|
*
Dead code from August 2014 in apply in.
Hugo Herbelin
2015-12-02
|
*
Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.
Hugo Herbelin
2015-12-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Fixing the "parsing rules with idents later declared as keywords" problem.
Hugo Herbelin
2015-11-26
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Adding syntax "Show id" to show goal named id (shelved or not).
Hugo Herbelin
2015-11-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
|
\
|
|
*
Manually expand red_tactic so that notations do not break reduction tactics. ...
Guillaume Melquiond
2015-10-30
|
*
Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)
Guillaume Melquiond
2015-10-29
*
|
Fixing the return type of the Atoken symbol.
Pierre-Marie Pédrot
2015-10-28
*
|
Removing unused code in Pcoq.
Pierre-Marie Pédrot
2015-10-27
*
|
Type-safe Egramml.grammar_prod_item.
Pierre-Marie Pédrot
2015-10-27
*
|
Finer type for Pcoq.interp_entry_name.
Pierre-Marie Pédrot
2015-10-27
*
|
Getting rid of most uses of unsafe_grammar_extend.
Pierre-Marie Pédrot
2015-10-27
*
|
Type-safe Egramml.make_rule.
Pierre-Marie Pédrot
2015-10-27
*
|
Indexing existentially quantified entries returned by interp_entry_name.
Pierre-Marie Pédrot
2015-10-27
*
|
Type-safe grammar extensions.
Pierre-Marie Pédrot
2015-10-27
*
|
Pcoq entries are given a proper module.
Pierre-Marie Pédrot
2015-10-26
*
|
Getting rid of the Atactic entry.
Pierre-Marie Pédrot
2015-10-25
*
|
Getting rid of the Agram entry.
Pierre-Marie Pédrot
2015-10-25
*
|
Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.
Pierre-Marie Pédrot
2015-10-21
*
|
Turn Pcoq into a regular ML file.
Pierre-Marie Pédrot
2015-10-21
*
|
Expanding the grammar extensions of Pcoq.
Pierre-Marie Pédrot
2015-10-21
*
|
Removing the dependencies of Pcoq in IFDEF macros.
Pierre-Marie Pédrot
2015-10-21
*
|
Expliciting some uses of Compat module.
Pierre-Marie Pédrot
2015-10-21
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-10-14
|
*
Fix some typos.
Guillaume Melquiond
2015-10-13
[next]