diff options
Diffstat (limited to 'contrib/correctness')
| -rw-r--r-- | contrib/correctness/ptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index a4b62c53c4..66633277a9 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -220,7 +220,7 @@ let correctness s p opttac = let env = Global.env () in let sign = Global.named_context () in let sigma = Evd.empty in - let cty = Reduction.nf_betaiota env sigma cty in + let cty = Reduction.nf_betaiota cty in let id = id_of_string s in start_proof id Declare.NeverDischarge sign cty; Penv.new_edited id (v,p); |