]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cic.ml
* env renamed to context everywhere in cicTypeChecker.ml
[helm.git] / helm / ocaml / cic / cic.ml
index 64b7f857cce087cc7f5925654939c2a613768434..0a43c4c571e80021fb625906c3d72a590442ddb6 100644 (file)
@@ -144,3 +144,11 @@ and 'a exactness =
    Possible of 'a                            (* an approximation to something *)
  | Actual of 'a                              (* something *)
 ;;
+
+(* Contexts are lists of context_entry *)
+type context_entry =
+   Decl of term
+ | Def of term
+;;
+
+type context = context_entry list;;