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
...
*
|
|
Moving Print Ltac to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Moving Tactic Notation to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Moving Tacinterp to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Fixing compilation with old versions of CAMLP5.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Further reducing the dependencies of the EXTEND macros.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Moving VernacSolve to an EXTEND-based definition.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Moving the parsing of the Ltac proof mode to G_ltac.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Moving the proof mode parsing management to Pcoq.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Allowing generalized rules in typed symbols.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Do not export entry_key from Pcoq anymore.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Simplifying the code of Entry.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Removing dead code in Pcoq.
Pierre-Marie Pédrot
2016-03-18
*
|
|
Making the EXTEND macros almost self-contained.
Pierre-Marie Pédrot
2016-03-18
*
|
|
ARGUMENT EXTEND made of only one entry share the same grammar.
Pierre-Marie Pédrot
2016-03-18
*
|
|
Removing the special status of generic arguments defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Code factorization in Pcoq.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Adding a universe argument to Pcoq.create_generic_entry.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Relying on parsing rules rather than genarg to check if an argument is empty.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Adopting the same rules for interpreting @, abbreviations and
Hugo Herbelin
2016-03-13
*
|
|
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Hugo Herbelin
2016-03-13
*
|
|
Moving Autorewrite to Hightatctic.
Pierre-Marie Pédrot
2016-03-06
*
|
|
Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.
Pierre-Marie Pédrot
2016-03-06
*
|
|
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
[prev]
[next]