diff src/elab_util.sig @ 329:eec65c11d3e2

foldTR2
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 10:30:45 -0400
parents e86411f647c6
children 85819353a84f
line wrap: on
line diff
--- a/src/elab_util.sig	Thu Sep 11 19:59:31 2008 -0400
+++ b/src/elab_util.sig	Sat Sep 13 10:30:45 2008 -0400
@@ -38,7 +38,7 @@
 structure Con : sig
     datatype binder =
              Rel of string * Elab.kind
-           | Named of string * Elab.kind
+           | Named of string * int * Elab.kind
 
     val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
                     con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
@@ -62,7 +62,7 @@
 structure Exp : sig
     datatype binder =
              RelC of string * Elab.kind
-           | NamedC of string * Elab.kind
+           | NamedC of string * int * Elab.kind
            | RelE of string * Elab.con
            | NamedE of string * Elab.con
 
@@ -88,7 +88,7 @@
 structure Sgn : sig
     datatype binder =
              RelC of string * Elab.kind
-           | NamedC of string * Elab.kind
+           | NamedC of string * int * Elab.kind
            | Str of string * Elab.sgn
            | Sgn of string * Elab.sgn
 
@@ -117,7 +117,7 @@
 structure Decl : sig
     datatype binder =
              RelC of string * Elab.kind
-           | NamedC of string * Elab.kind
+           | NamedC of string * int * Elab.kind
            | RelE of string * Elab.con
            | NamedE of string * Elab.con
            | Str of string * Elab.sgn