index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
refine.ml
Commit message (
Expand
)
Author
Age
*
proofview: goals come with a state
Enrico Tassi
2018-02-20
*
[engine] Remove ghost parameter from `Proofview.Goal.t`
Emilio Jesus Gallego Arias
2018-02-12
*
Fix a refine anomaly "Evar defined twice".
Pierre-Marie Pédrot
2017-09-06
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
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-13
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Merge PR#608: Allow Ltac2 as a plugin
Maxime Dénès
2017-05-25
|
\
|
*
Generalizing the refine primitive so as to accept tactic arguments.
Pierre-Marie Pédrot
2017-05-03
*
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
|
/
*
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
|
\
*
|
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
*
|
Proofview.Goal primitive now return EConstrs.
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
2017-02-14
*
|
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Coercion API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Typing API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-18
|
/
|
|
*
Renamings to avoid confusion deprecating old names
Matthieu Sozeau
2016-10-22
|
*
Unification constraint handling (#4763, #5149)
Matthieu Sozeau
2016-10-22
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-12
|
\
|
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-12
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-23
|
\
|
|
*
Adding variants enter_one and refine_one which assume that exactly one
Hugo Herbelin
2016-09-16
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-02
|
\
|
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-02
*
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
/
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Moving Refine to its proper module.
Pierre-Marie Pédrot
2016-03-20
Enrico Tassi
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Matthieu Sozeau
Hugo Herbelin
Matej Kosik