index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
comHints.ml
Age
Commit message (
Expand
)
Author
2020-12-21
Move evaluable_global_reference from Names to Tacred.
Pierre-Marie Pédrot
2020-11-04
Further code simplification in arbitrary hint interpretation.
Pierre-Marie Pédrot
2020-11-04
Do not try to be clever for term-as-hint interpretation.
Pierre-Marie Pédrot
2020-11-04
Opacify the Hints.hint_term type.
Pierre-Marie Pédrot
2020-11-04
Encapsulate the last use of IsConstr in the Hints API.
Pierre-Marie Pédrot
2020-09-13
Statically ensure that only polymophic hint terms come with a context.
Pierre-Marie Pédrot
2020-07-26
Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque Define...
Pierre-Marie Pédrot
2020-07-23
Hint Opaque/Transparent/Unfold: don't error on opaque constants
Gaëtan Gilbert
2020-07-17
Tweak the warning for arbitrary term hints.
Pierre-Marie Pédrot
2020-06-26
[declare] [api] Removal of duplicated type aliases.
Emilio Jesus Gallego Arias
2020-05-10
No more local reduction functions in Reductionops.
Pierre-Marie Pédrot
2020-05-07
[declare] Merge DeclareDef into Declare
Emilio Jesus Gallego Arias
2020-04-21
[declare] [tactics] Move declare to `vernac`
Emilio Jesus Gallego Arias
2020-04-21
[hints] Move and split Hint Declaration AST to vernac
Emilio Jesus Gallego Arias
