summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_interp_fixpoint.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /contrib/subtac/subtac_interp_fixpoint.mli
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'contrib/subtac/subtac_interp_fixpoint.mli')
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.mli39
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