diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 973bac719..3a6d68115 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -31,6 +31,17 @@ type fix_kind = RFix of (int array * int) | RCoFix of int type binder_kind = BProd | BLambda | BLetIn +type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier + +type 'a explicit_substitution = (quantified_hypothesis * 'a) list + +type 'a substitution = + | ImplicitBindings of 'a list + | ExplicitBindings of 'a explicit_substitution + | NoBindings + +type 'a with_bindings = 'a * 'a substitution + type hole_kind = | ImplicitArg of global_reference * int | AbstractionType of name @@ -81,3 +92,30 @@ val dummy_loc : loc val loc_of_rawconstr : rawconstr -> loc val set_loc_of_rawconstr : loc -> rawconstr -> rawconstr val join_loc : loc -> loc -> loc + +type 'a raw_red_flag = { + rBeta : bool; + rIota : bool; + rZeta : bool; + rDelta : bool; (* true = delta all but rConst; false = delta only on rConst*) + rConst : 'a list +} + +type ('a,'b) red_expr_gen = + | Red of bool + | Hnf + | Simpl + | Cbv of 'b raw_red_flag + | Lazy of 'b raw_red_flag + | Unfold of (int list * 'b) list + | Fold of 'a list + | Pattern of (int list * 'a) list + | ExtraRedExpr of string * 'a list + +type 'a or_metanum = AN of loc * 'a | MetaNum of loc * int + +type 'a may_eval = + | ConstrTerm of 'a + | ConstrEval of ('a, qualid or_metanum) red_expr_gen * 'a + | ConstrContext of (loc * identifier) * 'a + | ConstrTypeOf of 'a |