]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nReference.mli
Very experimental commit: the type of the source is now required in LetIns
[helm.git] / helm / software / components / ng_kernel / nReference.mli
index 116e30ac95bce6610147b2288383d1c692569979..1904f99c941a80fd9ff488df61d670c4c78a1bbd 100644 (file)
@@ -33,7 +33,7 @@ type spec =
  | Ind of int
  | Con of int * int (* indtyno, constrno *)
 
-type reference = Ref of int *  string * spec
+type reference = Ref of int *  NUri.uri * spec
 
 val eq: reference -> reference -> bool
 val string_of_reference: reference -> string