diff options
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 4238d1e372..8af28b6ab1 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -212,7 +212,7 @@ module New = struct let hyps = Proofview.Goal.hyps gl in List.hd hyps - let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) = + let pf_nf_concl (gl : ([ `LZ ], 'r) Proofview.Goal.t) = (** We normalize the conclusion just after *) let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in |