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
*
Removing the Entry module now that rules need not be marshalled.
Pierre-Marie Pédrot
2016-05-10
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
|
\
|
*
Rename Lexer -> CLexer.
Pierre-Marie Pédrot
2016-05-09
*
|
Interpretation function can return any untyped value.
Pierre-Marie Pédrot
2016-05-04
*
|
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
*
|
Adding warnings for inferrable *_TYPED AS clauses.
Pierre-Marie Pédrot
2016-04-12
*
|
Allowing optional RAW_TYPED and GLOB_TYPED clauses in ARGUMENT EXTEND.
Pierre-Marie Pédrot
2016-04-12
*
|
Warning for redundant TYPED AS clauses.
Pierre-Marie Pédrot
2016-04-12
*
|
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
|
*
Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".
Pierre-Marie Pédrot
2016-03-05
*
|
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
[next]