]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCic.ml
uri -> reference
[helm.git] / helm / software / components / ng_kernel / nCic.ml
index 6466912a14f2227dbdee060a48137b9aebd0080b..9221ba8d4bd0ab336cccc03779002dc7acc5bb69 100644 (file)
@@ -43,10 +43,10 @@ and term =
  | Prod     of name * term * term                     (* binder, source, target          *)
  | Lambda   of name * term * term                     (* binder, source, target          *)
  | LetIn    of name * term * term * term              (* binder, type, term, body        *)
- | Const    of NUriManager.uri                         (* uri contains indtypeno/constrno *)
+ | Const    of NUriManager.reference                         (* reference contains indtypeno/constrno *)
  | Sort     of sort                                   (* sort                            *)
  | Implicit of implicit_annotation                    (* ... *)
- | MutCase  of NUriManager.uri *                      (* ind. uri,             *)
+ | MutCase  of NUriManager.reference *                      (* ind. reference,             *)
     term * term *                                   (*  outtype, ind. term   *)
     term list                                       (*  patterns             *)