index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
proofs
/
refine.mli
Age
Commit message (
Expand
)
Author
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-05-29
[proofs] Remove unused API [detected by coverage]
Emilio Jesus Gallego Arias
2019-05-23
Fixing typos - Part 3
JPR
2019-02-05
Make Program a regular attribute
Maxime Dénès
2018-09-29
Replacing Refine.pr_constr by Termops.Internal.print_constr.
Hugo Herbelin
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-12
[engine] Remove ghost parameter from `Proofview.Goal.t`
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-13
Dualize the unsafe flag of refine into typecheck and make it mandatory.
Pierre-Marie Pédrot
2017-06-13
Turn the default behaviour of the refine primitive into the safe one.
Pierre-Marie Pédrot
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-05-19
Removing unused warnings.
Pierre-Marie Pédrot
2017-05-03
Generalizing the refine primitive so as to accept tactic arguments.
Pierre-Marie Pédrot
2017-02-14
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
Refine API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Making judgment type generic over the type of inner constrs.
Pierre-Marie Pédrot
2016-10-22
Unification constraint handling (#4763, #5149)
Matthieu Sozeau
2016-09-16
Adding variants enter_one and refine_one which assume that exactly one
Hugo Herbelin
2016-06-09
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-03-20
Moving Refine to its proper module.
Pierre-Marie Pédrot
