diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /checker/term.mli | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'checker/term.mli')
-rw-r--r-- | checker/term.mli | 20 |
1 files changed, 6 insertions, 14 deletions
diff --git a/checker/term.mli b/checker/term.mli index 1367e581..0340c79b 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -12,7 +12,7 @@ type case_printing = { ind_nargs : int; style : case_style; } type case_info = { ci_ind : inductive; ci_npar : int; - ci_cstr_nargs : int array; + ci_cstr_ndecls : int array; ci_pp_info : case_printing; } type contents = Pos | Null @@ -73,14 +73,6 @@ val subst1 : constr -> constr -> constr type named_declaration = identifier * constr option * constr type rel_declaration = name * constr option * constr -val map_named_declaration : - (constr -> constr) -> named_declaration -> named_declaration -val map_rel_declaration : - (constr -> constr) -> rel_declaration -> rel_declaration -val fold_named_declaration : - (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a -val fold_rel_declaration : - (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a type named_context = named_declaration list val empty_named_context : named_context val fold_named_context : @@ -111,8 +103,8 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool val eq_constr : constr -> constr -> bool (* Validation *) -val val_sortfam : Obj.t -> unit -val val_sort : Obj.t -> unit -val val_constr : Obj.t -> unit -val val_rctxt : Obj.t -> unit -val val_nctxt : Obj.t -> unit +val val_sortfam : Validate.func +val val_sort : Validate.func +val val_constr : Validate.func +val val_rctxt : Validate.func +val val_nctxt : Validate.func |