index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
/
proofview.mli
Commit message (
Expand
)
Author
Age
*
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
*
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
|
\
*
|
Do not ask for a normalized goal to get hypotheses and conclusions.
Pierre-Marie Pédrot
2017-02-14
*
|
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
|
Evar-normalizing functions now act on EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Proofview.Goal primitive now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
|
*
Proofview: tclINDEPENDENTL
Enrico Tassi
2017-02-10
|
*
Unification constraint handling (#4763, #5149)
Matthieu Sozeau
2016-10-22
|
/
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-12
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-12
*
Adding variants enter_one and refine_one which assume that exactly one
Hugo Herbelin
2016-09-16
*
Proofview: extensions for backtracking eauto
Matthieu Sozeau
2016-06-16
*
Implement limited proof search and iterative deepening.
Matthieu Sozeau
2016-06-16
*
Merge 'pr/191' into trunk
Enrico Tassi
2016-06-16
|
\
|
*
Fix a typo in proofs/proofview.mli.
Cyprien Mangin
2016-06-14
|
*
Add goal range selectors.
Cyprien Mangin
2016-06-14
*
|
STM: proof block detection for bullets and { block }
Enrico Tassi
2016-06-06
|
/
*
Moving Evarutil and Proofview to engine/
Pierre-Marie Pédrot
2016-03-20