summaryrefslogtreecommitdiff
path: root/checker/term.mli
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
commit9043add656177eeac1491a73d2f3ab92bec0013c (patch)
tree2b0092c84bfbf718eca10c81f60b2640dc8cab05 /checker/term.mli
parenta4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff)
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'checker/term.mli')
-rw-r--r--checker/term.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/checker/term.mli b/checker/term.mli
index 0af83e05..2524dff1 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -4,8 +4,6 @@ open Cic
val family_of_sort : sorts -> sorts_family
val family_equal : sorts_family -> sorts_family -> bool
-val strip_outer_cast : constr -> constr
-val collapse_appl : constr -> constr
val decompose_app : constr -> constr * constr list
val applist : constr * constr list -> constr
val iter_constr_with_binders :
@@ -35,11 +33,13 @@ val rel_context_length : rel_context -> int
val rel_context_nhyps : rel_context -> int
val fold_rel_context :
(rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val fold_rel_context_outside :
+ (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration
val map_rel_context : (constr -> constr) -> rel_context -> rel_context
val extended_rel_list : int -> rel_context -> constr list
-val compose_lam : (name * constr) list -> constr -> constr
-val decompose_lam : constr -> (name * constr) list * constr
+val compose_lam : (Name.t * constr) list -> constr -> constr
+val decompose_lam : constr -> (Name.t * constr) list * constr
val decompose_lam_n_assum : int -> constr -> rel_context * constr
val mkProd_or_LetIn : rel_declaration -> constr -> constr
val it_mkProd_or_LetIn : constr -> rel_context -> constr