diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-19 22:49:25 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:01:14 +0100 |
| commit | ade2363e357db3ac3f258e645fe6bba988e7e7dd (patch) | |
| tree | ade794510151d080d164be6d33d03aacbbe5064f /engine | |
| parent | f66e604a9d714ee9dba09234d935ee208bc89d97 (diff) | |
About building of substitutions from instances.
Redefining adjust_subst_to_rel_context from instantiate_context who
was hidden in inductiveops.ml, renamed the latter into
subst_of_rel_context_instance and moving them to Vars. The new name
highlights that the input is an instance (as for applist) and the
output a substitution (as for substl). This is a clearer unified
interface, centralizing the difficult de-Bruijn job in one place. It
saves a couple of List.rev.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 10 | ||||
| -rw-r--r-- | engine/termops.mli | 2 |
2 files changed, 1 insertions, 11 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 5716a19dd..63baec129 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -953,16 +953,6 @@ let smash_rel_context sign = aux (List.rev (substl_rel_context [b] (List.rev acc))) l in List.rev (aux [] sign) -let adjust_subst_to_rel_context sign l = - let rec aux subst sign l = - match sign, l with - | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args' - | (_,Some c,_)::sign', args' -> - aux (substl subst c :: subst) sign' args' - | [], [] -> List.rev subst - | _ -> anomaly (Pp.str "Instance and signature do not match") - in aux [] (List.rev sign) l - let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let rec mem_named_context id = function diff --git a/engine/termops.mli b/engine/termops.mli index 5d812131e..94c485a26 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -219,7 +219,7 @@ val assums_of_rel_context : rel_context -> (Name.t * 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 : |