diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0645a87f0..6a282d547 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1131,7 +1131,7 @@ let interp c = match c with | VernacNotation (inf,c,pl,sc) -> vernac_notation inf c pl sc (* Gallina *) - | VernacDefinition (k,id,d,f) -> vernac_definition k id d f + | VernacDefinition (k,id,d,f,_) -> vernac_definition k id d f | VernacStartTheoremProof (k,id,t,top,f) -> vernac_start_proof k (Some id) t top f | VernacEndProof (opaq,idopt) -> vernac_end_proof opaq idopt |