diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 10:37:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 15:43:33 +0200 |
| commit | 67b8fba4209c407c94ed8d54ec78352397d82f59 (patch) | |
| tree | 5c78c966e95f957002f55ebd2e09ea7bebab83d8 /proofs/goal.ml | |
| parent | 3806d567af6b1feee2c8f196199eee4208a8551d (diff) | |
Proofview refiner is now type-safe by default.
In order not to be too costly, there is an [unsafe] flag to be set if the
tactic does not have to check that the partial proof term is well-typed (to
be used with caution though).
This patch breaks one [fix]-based example in the refine test-suite, but a huge
development like CompCert still goes through.
Diffstat (limited to 'proofs/goal.ml')
0 files changed, 0 insertions, 0 deletions