index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
taccoerce.ml
Commit message (
Expand
)
Author
Age
*
Finer-grained types for toplevel values.
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
*
Fixing compilation for 3.12.
Pierre-Marie Pédrot
2015-02-12
*
Tentative fix for bug #4027.
Pierre-Marie Pédrot
2015-02-12
*
Update headers.
Maxime Dénès
2015-01-12
*
Moving the decompose tactic out of the AST.
Pierre-Marie Pédrot
2014-09-01
*
Type-safe version of genarg list / pair / opt functions.
Pierre-Marie Pédrot
2014-08-29
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
[uconstr]: use a closure instead of eager substitution.
Arnaud Spiwack
2014-08-06
*
Removing "intros untils" from the AST.
Pierre-Marie Pédrot
2014-08-06
*
Faster uconstr.
Arnaud Spiwack
2014-08-01
*
Untyped terms in ltac: simplify [coerce_to_uconstr].
Arnaud Spiwack
2014-08-01
*
Untyped terms in tactic: add the possibility to use a typed term inside an un...
Arnaud Spiwack
2014-07-29
*
Add a type of untyped term to Ltac's value.
Arnaud Spiwack
2014-07-29
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-07-05
*
Removed the distinction between generic Ltac vars and Let/Intro
ppedrot
2013-06-27
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
*
Moving wit_unit to Stdarg.
ppedrot
2013-06-19
*
Proof-of-concept: moved four easy-to-handle generic arguments to
ppedrot
2013-06-18
*
Normalizing exception raised by tactic coercions.
ppedrot
2013-06-13
*
Moving coercion functions out of Tacinterp.
ppedrot
2013-06-12