index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
lib
/
genarg.ml
Age
Commit message (
Expand
)
Author
2015-12-21
Finer-grained types for toplevel values.
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
Sharing toplevel representation for several generic types.
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
Attaching a dynamic argument to the toplevel type of generic arguments.
Pierre-Marie Pédrot
2015-12-17
Getting rid of some hardwired generic arguments.
Pierre-Marie Pédrot
2015-12-12
Removing dead unsafe code in Genarg.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-08-29
Type-safe version of genarg list / pair / opt functions.
Pierre-Marie Pédrot
2014-08-29
Simplification of Genarg unpackers.
Pierre-Marie Pédrot
2014-03-05
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-02-27
Remove unsafe code (Obj.magic) in Tacinterp.
Arnaud Spiwack
2014-01-19
Adding a default object to generic argument registering mechanism.
Pierre-Marie Pédrot
2013-12-19
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-01
Removing RefArgType generic argument.
Pierre-Marie Pédrot
2013-11-30
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-08-04
Small cleaning of printing coercion failures in Ltac interpretation.
ppedrot
2013-07-05
Removing SortArgType.
ppedrot
2013-07-05
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-06-30
Using functors to reduce the boilerplate used in registering
ppedrot
2013-06-27
Getting rid of IntroPatternArgType.
ppedrot
2013-06-21
Splitted up Genarg in four different levels:
ppedrot
