]
type literal =
- [ `Symbol of string
- | `Keyword of string
- | `Number of string
+ [ `Symbol of string * (string option * string option)
+ | `Keyword of string * (string option * string option)
+ | `Number of string * (string option * string option)
]
type case_indtype = string * href option
(** To be increased each time the term type below changes, used for "safe"
* marshalling *)
-let magic = 7
+let magic = 8
type term =
(* CIC AST *)
| NCic of NCic.term
(* Syntax pattern extensions *)
-
- | Literal of literal
+ (* string option = optional name of an Ast.Symbol occurring in the level 2
+ * term, which is associated to this literal *)
+ | Literal of (string option * literal)
| Layout of layout_pattern
| Magic of magic_term
| Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
(** left parameters, name, type, fields *)
+let name_of_obj = function
+ | Theorem (_,n,_,_,_) | Record (_,n,_,_)
+ | Inductive (_,(n,_,_,_)::_) -> n
+ | _ -> (* empty inductive block *) assert false
+;;
+
let map_variable f (t,u) = f t, HExtlib.map_option f u ;;
let map_pattern f = function
let apply_prec = 70
let simple_prec = 90
+(* sequents *)
+
+type context_entry =
+ Decl of term
+ | Def of term * term
+
+type sequent = int * context * term
+and context = (string * context_entry) list