diff options
| author | herbelin | 2009-08-11 15:15:46 +0000 |
|---|---|---|
| committer | herbelin | 2009-08-11 15:15:46 +0000 |
| commit | a07e31a2693bde01d3dca59364693096d550561a (patch) | |
| tree | 322e0acb77a7dfc1a2276b88a73357ffc09a08a7 /pretyping/termops.mli | |
| parent | 9cfe880e1f5f9dddd63aa269a2fb159665c2d182 (diff) | |
Ensures that let-in's in arities of inductive types work well. Maybe not
very useful in practice but as soon as let-in's were not forbidden in
the internal data structure, better to do it. Moreover, this gets
closer to the view were inductive definitions are uniformly built from
"contexts". (checker not changed!)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index f9d4329077..3d167ebb03 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -267,6 +267,8 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env val assums_of_rel_context : rel_context -> (name * constr) list val lift_rel_context : int -> rel_context -> rel_context val substl_rel_context : constr list -> rel_context -> rel_context +val smash_rel_context : rel_context -> rel_context (* expand lets in context *) +val adjust_subst_to_rel_context : rel_context -> constr list -> constr list val map_rel_context_in_env : (env -> constr -> constr) -> env -> rel_context -> rel_context val map_rel_context_with_binders : |