index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
stdarg.mli
Age
Commit message (
Expand
)
Author
2020-11-20
Use nat_or_var where negative values don't make sense
Jim Fehrle
2020-10-14
Deprecating wit_var to the benefit of its synonymous wit_hyp.
Hugo Herbelin
2020-09-11
Adding a wit_natural standard argument.
Hugo Herbelin
2020-05-09
Add a `with_strategy` tactic
Jason Gross
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2018-12-11
[api] Move reduction modules to `tactics`
Emilio Jesus Gallego Arias
2018-06-18
Remove reference name type.
Maxime Dénès
2018-06-12
[api] Remove Misctypes.
Emilio Jesus Gallego Arias
2018-06-12
[api] Misctypes removal: move Tactypes to proofs
Emilio Jesus Gallego Arias
2018-05-04
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-03-09
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-03-09
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-22
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2017-10-25
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-09-08
Parse directly to Sorts.family when appropriate.
Gaëtan Gilbert
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-05-25
Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings
Maxime Dénès
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-22
Clarifying the interpretation path for the "constr_with_binding" argument.
Hugo Herbelin
2017-04-27
Remove unused [open] statements
Gaetan Gilbert
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-02-14
Ltac now uses evar-based constrs.
Pierre-Marie Pédrot
2017-02-14
Tactics API using EConstr.
Pierre-Marie Pédrot
2016-09-21
Merging Stdarg and Constrarg.
Pierre-Marie Pédrot
2016-03-17
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2013-06-19
Moving wit_unit to Stdarg.
ppedrot
2013-06-18
Proof-of-concept: moved four easy-to-handle generic arguments to
ppedrot
