index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
egramcoq.mli
Commit message (
Expand
)
Author
Age
*
Removing the use to Egramcoq.recover_constr_grammar.
Pierre-Marie Pédrot
2016-06-07
*
Moving the grammar summary to Pcoq.
Pierre-Marie Pédrot
2016-05-11
*
Moving the code handling tactic notations to Tacentries.
Pierre-Marie Pédrot
2016-03-31
*
Abstracting away the Summary-synchronized grammar-modifying commands.
Pierre-Marie Pédrot
2016-03-31
*
Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].
Pierre-Marie Pédrot
2016-03-04
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Indexing existentially quantified entries returned by interp_entry_name.
Pierre-Marie Pédrot
2015-10-27
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
Moving the TacExtend node from atomic to plain tactics.
Pierre-Marie Pédrot
2014-08-18
*
Qualified ML tactic names. The plugin name is used to discriminate
Pierre-Marie Pédrot
2014-07-27
*
Moving the ML tactic extension mechanism to a Libobject-based one.
Pierre-Marie Pédrot
2014-05-12
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
ppedrot
2013-11-10
*
Revert the previous commit. It broke Coq compilation.
ppedrot
2013-11-09
*
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
ppedrot
2013-11-09
*
Moving notation types into grammar rule.
ppedrot
2013-11-09
*
Cleaning and documenting Egramcoq.
ppedrot
2013-11-09
*
Added a generic handler of Ltac quotations, based on the existing
ppedrot
2013-06-27
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Adding a nominal typing layer to Metasyntax in order to clarify
ppedrot
2012-10-04
*
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
2012-10-04
*
Updating headers.
herbelin
2012-08-08
*
Split Egrammar into Egramml and Egramcoq
letouzey
2012-05-29