index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
hints.ml
Age
Commit message (
Expand
)
Author
2015-05-13
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-12
Adding an option Loose Hint Behavior to handle hints loaded but not imported.
Pierre-Marie Pédrot
2015-05-12
Adding unique identifiers to hints.
Pierre-Marie Pédrot
2015-05-11
Rationalizing a bit the interface of Hints.
Pierre-Marie Pédrot
2015-04-23
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-16
Ensuring purity of datastructures in the API.
Pierre-Marie Pédrot
2015-04-14
Cleaning up the implementation of search entries in Hints.
Pierre-Marie Pédrot
2015-04-14
Opaque implementation of auto tactics.
Pierre-Marie Pédrot
2015-04-13
More documented representation of hint objects.
Pierre-Marie Pédrot
2015-03-03
Fix bug #3590, keeping evars that are not turned into named metas by
Matthieu Sozeau
2015-01-12
Update headers.
Maxime Dénès
2014-10-27
Removing the last Evd.diff from Hints.
Pierre-Marie Pédrot
2014-10-08
Forgotten hints.ml{,i} files in 38b34dfffcc.
Hugo Herbelin
