From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- checker/term.mli | 20 ++++++-------------- 1 file changed, 6 insertions(+), 14 deletions(-) (limited to 'checker/term.mli') 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 -- cgit v1.2.3