From a6d534b172ccb8eadc24e0e903b196085869800e Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Fri, 28 Mar 2008 15:20:46 -0400
Subject: Simple elaboration working

---
 src/elab_env.sml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src/elab_env.sml')

diff --git a/src/elab_env.sml b/src/elab_env.sml
index 2199ccbe..27ea1750 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -50,7 +50,7 @@ datatype 'a var =
 type env = {
      renameC : kind var' SM.map,
      relC : (string * kind) list,
-     namedC : (string * kind) IM.map,
+     namedC : (string * kind * con option) IM.map,
 
      renameE : con var' SM.map,
      relE : (string * con) list,
@@ -87,21 +87,21 @@ fun lookupCRel (env : env) n =
     (List.nth (#relC env, n))
     handle Subscript => raise UnboundRel n
 
-fun pushCNamedAs (env : env) x n k =
+fun pushCNamedAs (env : env) x n k co =
     {renameC = SM.insert (#renameC env, x, Named' (n, k)),
      relC = #relC env,
-     namedC = IM.insert (#namedC env, n, (x, k)),
+     namedC = IM.insert (#namedC env, n, (x, k, co)),
 
      renameE = #renameE env,
      relE = #relE env,
      namedE = #namedE env}
 
-fun pushCNamed env x k =
+fun pushCNamed env x k co =
     let
         val n = !namedCounter
     in
         namedCounter := n + 1;
-        (pushCNamedAs env x n k, n)
+        (pushCNamedAs env x n k co, n)
     end
 
 fun lookupCNamed (env : env) n =
-- 
cgit v1.2.3