diff options
| author | Matej Kosik | 2016-02-17 11:16:27 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-02-17 11:16:27 +0100 |
| commit | 93c03652fea5914307b0a6b72b7fec6f9aaec305 (patch) | |
| tree | fe9e5e983452d5489550e9322d42067e4b213e19 /kernel/vars.ml | |
| parent | 06fa0334047a9400d0b5a144601fca35746a53b8 (diff) | |
| parent | 1dddd062f35736285eb2940382df2b53224578a7 (diff) | |
CLEANUP: Context.{Rel,Named}.Declaration.t
Diffstat (limited to 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index 4554c6be17..b935ab6b91 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -8,6 +8,7 @@ open Names open Esubst +open Context.Rel.Declaration (*********************) (* Occurring *) @@ -159,17 +160,17 @@ let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c -let substnl_decl laml k r = Context.Rel.Declaration.map (fun c -> substnl laml k c) r -let substl_decl laml r = Context.Rel.Declaration.map (fun c -> substnl laml 0 c) r -let subst1_decl lam r = Context.Rel.Declaration.map (fun c -> subst1 lam c) r +let substnl_decl laml k r = map_constr (fun c -> substnl laml k c) r +let substl_decl laml r = map_constr (fun c -> substnl laml 0 c) r +let subst1_decl lam r = map_constr (fun c -> subst1 lam c) r (* Build a substitution from an instance, inserting missing let-ins *) let subst_of_rel_context_instance 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' -> + | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args' + | LocalDef (_,c,_)::sign', args' -> aux (substl subst c :: subst) sign' args' | [], [] -> subst | _ -> Errors.anomaly (Pp.str "Instance and signature do not match") |