comparison src/elab_err.sig @ 1000:5d7e05b4a5c0

Better subSgn error locations
author Adam Chlipala <adamc@hcoop.net>
date Thu, 15 Oct 2009 14:27:38 -0400
parents cb30dd2ba353
children 26197c957ad6
comparison
equal deleted inserted replaced
999:8d821baac99e 1000:5d7e05b4a5c0
86 86
87 val declError : ElabEnv.env -> decl_error -> unit 87 val declError : ElabEnv.env -> decl_error -> unit
88 88
89 datatype sgn_error = 89 datatype sgn_error =
90 UnboundSgn of ErrorMsg.span * string 90 UnboundSgn of ErrorMsg.span * string
91 | UnmatchedSgi of Elab.sgn_item 91 | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
92 | SgiWrongKind of Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error 92 | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
93 | SgiWrongCon of Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error 93 | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
94 | SgiMismatchedDatatypes of Elab.sgn_item * Elab.sgn_item * (Elab.con * Elab.con * cunify_error) option 94 | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
95 | SgnWrongForm of Elab.sgn * Elab.sgn 95 * (Elab.con * Elab.con * cunify_error) option
96 | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
96 | UnWhereable of Elab.sgn * string 97 | UnWhereable of Elab.sgn * string
97 | WhereWrongKind of Elab.kind * Elab.kind * kunify_error 98 | WhereWrongKind of Elab.kind * Elab.kind * kunify_error
98 | NotIncludable of Elab.sgn 99 | NotIncludable of Elab.sgn
99 | DuplicateCon of ErrorMsg.span * string 100 | DuplicateCon of ErrorMsg.span * string
100 | DuplicateVal of ErrorMsg.span * string 101 | DuplicateVal of ErrorMsg.span * string