type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of
-CicUniv.universe | `NType of string |`NCProp of string]
+type sort_kind = [ `Prop | `Set | `NType of string |`NCProp of string]
type fold_kind = [ `Left | `Right ]
type location = Stdpp.location
let (x, y) = HExtlib.loc_of_floc floc in
failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
-type href = UriManager.uri
+type href = NReference.reference
type child_pos = [ `Left | `Right | `Inner ]
| IdentArg of int * string (* eta-depth, name *)
type cic_appl_pattern =
- | UriPattern of UriManager.uri
| NRefPattern of NReference.reference
| VarPattern of string
| ImplicitPattern
type 'term obj =
| Inductive of 'term capture_variable list * 'term inductive_type list
(** parameters, list of loc * mutual inductive types *)
- | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma
+ | Theorem of NCic.def_flavour * string * 'term * 'term option * NCic.def_pragma
(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage