diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-05-02 19:53:05 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:17 +0200 |
| commit | d6898781f9cd52ac36a4891d7b169ddab7b8af50 (patch) | |
| tree | 880ef0bcad043f083a6157644d10e068b8185b4c /checker/term.mli | |
| parent | 4bf85270a36a0a3f9517d8bce92d843f882af00a (diff) | |
Correct coqchk reduction
Diffstat (limited to 'checker/term.mli')
| -rw-r--r-- | checker/term.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/checker/term.mli b/checker/term.mli index 6b026d056..ccf5b59e0 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -33,6 +33,8 @@ 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 @@ -55,3 +57,4 @@ val eq_constr : constr -> constr -> bool (** Instance substitution for polymorphism. *) val subst_instance_constr : Univ.universe_instance -> constr -> constr val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context +val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr |