diff options
Diffstat (limited to 'contrib/subtac/subtac_interp_fixpoint.mli')
| -rw-r--r-- | contrib/subtac/subtac_interp_fixpoint.mli | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli new file mode 100644 index 00000000..b0de0641 --- /dev/null +++ b/contrib/subtac/subtac_interp_fixpoint.mli @@ -0,0 +1,39 @@ +val mkAppExplC : + Libnames.reference * Topconstr.constr_expr list -> Topconstr.constr_expr +val mkSubset : + Names.name Util.located -> + Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr +val mkProj1 : + Topconstr.constr_expr -> + Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr +val mkProj2 : + Topconstr.constr_expr -> + Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr +val list_of_local_binders : + Topconstr.local_binder list -> + (Names.name Util.located * Topconstr.constr_expr) list +val pr_binder_list : + (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds +val rewrite_rec_calls : 'a -> 'b -> 'b +val rewrite_fixpoint : + 'a -> + 'b -> + (Names.identifier * (int * Topconstr.recursion_order_expr) * + Topconstr.local_binder list * Topconstr.constr_expr * + Topconstr.constr_expr) * + 'c -> + (Names.identifier * (int * Topconstr.recursion_order_expr) * + Topconstr.local_binder list * Topconstr.constr_expr * + Topconstr.constr_expr) * + 'c +val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list +val rewrite_cases_aux : + Util.loc * Rawterm.rawconstr option * + (Rawterm.rawconstr * + (Names.name * (Util.loc * Names.inductive * Names.name list) option)) + list * + (Util.loc * Names.identifier list * Rawterm.cases_pattern list * + Rawterm.rawconstr) + list -> Rawterm.rawconstr + +val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr |