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

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