diff 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
line wrap: on
line diff
--- a/src/elab_err.sig	Mon Oct 12 18:17:57 2009 -0400
+++ b/src/elab_err.sig	Thu Oct 15 14:27:38 2009 -0400
@@ -88,11 +88,12 @@
 
     datatype sgn_error =
              UnboundSgn of ErrorMsg.span * string
-           | UnmatchedSgi of Elab.sgn_item
-           | SgiWrongKind of Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
-           | SgiWrongCon of Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
-           | SgiMismatchedDatatypes of Elab.sgn_item * Elab.sgn_item * (Elab.con * Elab.con * cunify_error) option
-           | SgnWrongForm of Elab.sgn * Elab.sgn
+           | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
+           | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
+           | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
+           | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
+                                       * (Elab.con * Elab.con * cunify_error) option
+           | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
            | UnWhereable of Elab.sgn * string
            | WhereWrongKind of Elab.kind * Elab.kind * kunify_error
            | NotIncludable of Elab.sgn