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 ]
(** To be increased each time the term type below changes, used for "safe"
* marshalling *)
-let magic = 6
+let magic = 8
type term =
(* CIC AST *)
(* what to match, inductive type, out type, <pattern,action> list *)
| Cast of term * term
| LetIn of term capture_variable * term * term (* name, body, where *)
- | LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term
- (* (params, name, body, decreasing arg) list, where *)
| Ident of string * subst list option
(* literal, substitutions.
* Some [] -> user has given an empty explicit substitution list
| 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 inductive_type = string * bool * 'term * (string * 'term) list
type 'term obj =
- | Inductive of 'term capture_variable list * 'term inductive_type list
+ | Inductive of 'term capture_variable list * 'term inductive_type list * NCic.source
(** parameters, list of loc * mutual inductive types *)
- | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma
- (** flavour, name, type, body
+ | Theorem of string * 'term * 'term option * NCic.c_attr
+ (** name, type, body, attributes
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
* - body is present when its given along with the command, otherwise it
* will be given in proof editing mode using the tactical language,
* unless the flavour is an Axiom
*)
- | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
+ | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list * NCic.source
(** left parameters, name, type, fields *)
+ | LetRec of induction_kind * ('term capture_variable list * 'term capture_variable * 'term * int) list * NCic.f_attr
+ (* (params, name, body, decreasing arg) list, attributes *)
(** {2 Standard precedences} *)
let binder_prec = 20
let apply_prec = 70
let simple_prec = 90
-