index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
grammar
/
argextend.ml4
Commit message (
Expand
)
Author
Age
*
Allowing simple ARGUMENT EXTEND not to mention their self type.
Pierre-Marie Pédrot
2016-04-12
*
Allowing the presence of TYPED AS in specialized ARGUMENT EXTEND.
Pierre-Marie Pédrot
2016-04-12
*
Moving the code handling tactic notations to Tacentries.
Pierre-Marie Pédrot
2016-03-31
*
EXTEND macros use their own internal representations.
Pierre-Marie Pédrot
2016-03-19
*
Do not keep the argument type in ExtNonTerminal.
Pierre-Marie Pédrot
2016-03-19
*
Further reducing the dependencies of the EXTEND macros.
Pierre-Marie Pédrot
2016-03-19
*
Do not export entry_key from Pcoq anymore.
Pierre-Marie Pédrot
2016-03-19
*
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
*
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
Adding a universe argument to Pcoq.create_generic_entry.
Pierre-Marie Pédrot
2016-03-17
*
Removing the registering of default values for generic arguments.
Pierre-Marie Pédrot
2016-03-17
*
Reducing the number of modules linked in grammar.cma.
Pierre-Marie Pédrot
2016-03-17
*
All arguments defined through ARGUMENT EXTEND declare a tactic scope.
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
*
|
ML extensions use untyped representation of user entries.
Pierre-Marie Pédrot
2016-01-17
*
|
Removing constr generic argument.
Pierre-Marie Pédrot
2016-01-14
*
|
Removing ident and var generic arguments.
Pierre-Marie Pédrot
2016-01-14
*
|
Monotonizing Ftactic.
Pierre-Marie Pédrot
2016-01-08
*
|
Proper datatype for EXTEND syntax tokens.
Pierre-Marie Pédrot
2016-01-02
*
|
Implementing non-focussed generic arguments.
Pierre-Marie Pédrot
2015-12-28
*
|
Removing the special status of open_constr generic argument.
Pierre-Marie Pédrot
2015-12-28
*
|
ARGUMENT EXTEND shares the toplevel representation when possible.
Pierre-Marie Pédrot
2015-12-21
*
|
Removing ad-hoc interpretation rules for tactic notations and their genarg.
Pierre-Marie Pédrot
2015-12-21
*
|
Removing the now useless genarg generic argument.
Pierre-Marie Pédrot
2015-12-21
*
|
Using dynamic values in tactic evaluation.
Pierre-Marie Pédrot
2015-12-21
*
|
Getting rid of some hardwired generic arguments.
Pierre-Marie Pédrot
2015-12-17
*
|
Type-safe Argextend.
Pierre-Marie Pédrot
2015-10-28
*
|
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
*
|
Indexing existentially quantified entries returned by interp_entry_name.
Pierre-Marie Pédrot
2015-10-27
*
|
Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.
Pierre-Marie Pédrot
2015-10-21
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-19
*
Removing RefArgType generic argument.
Pierre-Marie Pédrot
2013-12-01
*
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-30
*
Tacinterp: fewer use of old-style goals.
Arnaud Spiwack
2013-11-25
*
Removing SortArgType.
ppedrot
2013-07-05
*
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-07-05
*
Removed the ad-hod handling of wit_tacticn.
ppedrot
2013-07-02
*
Fixing Camlp4 compilation.
ppedrot
2013-06-30
*
Getting rid of IntroPatternArgType.
ppedrot
2013-06-27
*
Splitted up Genarg in four different levels:
ppedrot
2013-06-21
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
*
Fixing argument extension. Instead of qualified names, string
ppedrot
2013-06-19
*
Proof-of-concept: moved four easy-to-handle generic arguments to
ppedrot
2013-06-18
*
Removing the various glob/subst/interp registering functions for
ppedrot
2013-06-18
[next]