diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d7f8b8386..b2c5df74f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -434,6 +434,19 @@ let add_mind sp mie env = let add_constraints = add_constraints +let pop_vars idl env = + let rec remove n sign = + if n = 0 then + sign + else + match sign with + | (id::ids,_::tys) -> + if not (List.mem id idl) then anomaly "pop_vars"; + remove (pred n) (ids,tys) + | _ -> anomaly "pop_vars" + in + change_hyps (remove (List.length idl)) env + let export = export let import = import |