X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=0a43c4c571e80021fb625906c3d72a590442ddb6;hb=7db7305941a97d43480cf58c08a154ed79f300cb;hp=64b7f857cce087cc7f5925654939c2a613768434;hpb=797425e905a9d26bb21f18d234a34ed211bcf92c;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 64b7f857c..0a43c4c57 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -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;;