diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-03 18:16:21 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-04 10:25:55 +0200 |
| commit | a93104d5462894d5d0651aa2e04e12c311eb5897 (patch) | |
| tree | 8619451aa37d699fc012f0e5f6509560d9c46726 /stm/vernac_classifier.ml | |
| parent | 06e6a7b5a0d15f493a3f94fad905af2c44be9c09 (diff) | |
Remove [Infer] option of records.
Dead code formerly used by the now defunct [autoinstances].
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 5bbd857d9..ce9c2b3ff 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -134,7 +134,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in VtSideff ids, VtLater | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,_,l) -> + | VernacInductive (_,_,l) -> let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ |