type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
type fold_kind = [ `Left | `Right ]
type location = Lexing.position * Lexing.position
let (x, y) = loc_of_floc floc in
failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
+type href = UriManager.uri
+
type term_attribute =
[ `Loc of location (* source file location *)
| `IdRef of string (* ACic pointer *)
- | `Href of UriManager.uri list (* hyperlinks for literals *)
+ | `Href of href list (* hyperlinks for literals *)
| `Level of int * Gramext.g_assoc (* precedence, associativity *)
| `XmlAttrs of (string option * string * string) list
(* list of XML attributes: namespace, name, value *)
+ | `Raw of string (* unparsed version *)
]
type literal =
| `Number of string
]
+type case_indtype = string * href option
+
+(** To be increased each time the term type below changes, used for "safe"
+ * marshalling *)
+let magic = 1
+
type term =
(* CIC AST *)
| Appl of term list
| Binder of binder_kind * capture_variable * term (* kind, name, body *)
- | Case of term * string option * term option * (case_pattern * term) list
+ | Case of term * case_indtype option * term option *
+ (case_pattern * term) list
(* what to match, inductive type, out type, <pattern,action> list *)
| Cast of term * term
| LetIn of capture_variable * term * term (* name, body, where *)
and meta_subst = term option
and subst = string * term
-and case_pattern = string * capture_variable list
+and case_pattern = string * href option * capture_variable list
and box_kind = H | V | HV | HOV
and box_spec = box_kind * bool * bool (* kind, spacing, indent *)