index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
g_tactic.ml4
Age
Commit message (
Expand
)
Author
2017-07-25
[api] Remove type equalities from API.
Emilio Jesus Gallego Arias
2017-07-17
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-14
Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)
Pierre Letouzey
2017-06-10
Remove (useless) aliases from the API.
Matej Košík
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-05-30
Adding "epose", "eset", "eremember" which allow to set terms with
Hugo Herbelin
2017-05-30
Adding "eassert", "eenough", "epose proof", which allow to state
Hugo Herbelin
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-16
Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.
Hugo Herbelin
2017-04-25
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-24
[location] Use located in misctypes.
Emilio Jesus Gallego Arias
2017-04-24
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-07
[camlpX] Remove camlp4 compat layer.
Emilio Jesus Gallego Arias
2017-03-15
Attempt to improve error message when "apply in" fail.
Hugo Herbelin
2017-02-17
Ltac as a plugin.
Pierre-Marie Pédrot
