type implicit_annotation = [ `Closed | `Type | `Hole | `Term ]
-type local_context = int * (term list) option (* shift (0 -> no shift),
- subst (None means id) *)
+type lc_kind = Irl of int | Ctx of term list
+
+and local_context = int * lc_kind (* shift (0 -> no shift),
+ subst (None means id) *)
and term =
| Rel of int (* DeBruijn index, 1 based *)
| Meta of int * local_context
type metasenv = conjecture list
-type substitution = (int * (string option * context * term * term)) list
+type subst_entry = string option * context * term * term
+
+type substitution = (int * subst_entry) list
(******************************** OBJECTS **********************************)
| `Projection (* record projection *)
| `InversionPrinciple (* inversion principle *)
| `Variant
- | `Local ] (* Local = hidden technicality *)
+ | `Local
+ | `Regular ] (* Local = hidden technicality *)
type ind_pragma = (* pragmatic of the object *)
- [ `Record of (string * bool * int) list ]
+ [ `Record of (string * bool * int) list | `Regular ]
(* inductive type that encodes a record; the arguments are the record
* fields names and if they are coercions and then the coercion arity *)
type obj_kind =
| Constant of relevance * string * term option * term * c_attr
| Fixpoint of bool * inductiveFun list * f_attr
+ (* true -> fix, funcs, arrts *)
| Inductive of bool * int * inductiveType list * i_attr
- (* (co)inductive, leftno, types *)
+ (* true -> inductive, leftno, types *)
+ (* the int must be 0 if the object has no body *)
type obj = NUri.uri * int * metasenv * substitution * obj_kind