diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /checker/term.mli | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
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 |