diff src/elab_env.sig @ 171:c7a6e6dbc318

Elaborating some basic pattern matching
author Adam Chlipala <adamc@hcoop.net>
date Thu, 31 Jul 2008 10:06:27 -0400
parents b4b70de488e9
children 7ee424760d2f
line wrap: on
line diff
--- a/src/elab_env.sig	Tue Jul 29 16:38:15 2008 -0400
+++ b/src/elab_env.sig	Thu Jul 31 10:06:27 2008 -0400
@@ -54,9 +54,11 @@
     val pushDatatype : env -> int -> (string * int * Elab.con option) list -> env
     type datatyp
     val lookupDatatype : env -> int -> datatyp
-    val lookupConstructor : datatyp -> int -> string * Elab.con option
+    val lookupDatatypeConstructor : datatyp -> int -> string * Elab.con option
     val constructors : datatyp -> (string * int * Elab.con option) list
 
+    val lookupConstructor : env -> string -> (int * Elab.con option * int) option
+
     val pushERel : env -> string -> Elab.con -> env
     val lookupERel : env -> int -> string * Elab.con