From 40183da6b54d8deef242bac074079617d4a657c2 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 21 Jan 2000 18:42:22 +0000
Subject: gros commit de tout ce que j'ai fait pendant les vacances :  -
 tactics/Equality  - debug du discharge  - constr_of_compattern implante vite
 fait / mal fait en attendant mieux  - theories/Logic (ne passe pas
 entierrement)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'kernel/safe_typing.ml')

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
 
-- 
cgit v1.2.3