suppression de pop_named

meilleure discrimination dans les tactiques d'inversion


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 0 insertions, 13 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2cff2f7164..7113b4040e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -101,7 +101,6 @@ let named_context_app f env =
       env_named_context = f env.env_named_context }
 
 let push_named d   = named_context_app (Sign.add_named_decl d)
-let pop_named id         = named_context_app (Sign.pop_named_decl id)
 
 let reset_context env =
   { env with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index a7670f46e2..98f6380c06 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -53,7 +53,6 @@ val fold_rel_context :
 (***********************************************************************)
 (* Context of variables (section variables and goal assumptions) *)
 val push_named : named_declaration -> env -> env
-val pop_named  : identifier -> env -> env
 
 (* Looks up in the context of local vars referred by names ([named_context]) *)
 (* raises [Not_found] if the identifier is not found *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f284d774d9..ad36e2941b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -123,11 +123,6 @@ let add_mind sp mie env =
 
 let add_constraints = Environ.add_constraints
 
-let rec pop_named_decls idl env =
-  match idl with 
-    | [] -> env
-    | id::l -> pop_named_decls l (Environ.pop_named id env)
-
 let export = export
 let import = import
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 853bc7ccd9..071a67224a 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -32,7 +32,6 @@ val push_named_assum :
 val push_named_def :
   identifier * constr * types option -> safe_environment ->
     Univ.constraints * safe_environment
-val pop_named_decls : identifier list -> safe_environment -> safe_environment
 
 (* Adding global axioms or definitions *)
 type constant_entry = {
diff --git a/kernel/sign.ml b/kernel/sign.ml
index e1c9fbe4b0..8c05d15ca2 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -35,10 +35,6 @@ let add_named_decl (id,_,_ as d) sign =
 
 let named_context_length = List.length
 
-let pop_named_decl id = function
-  | (id',_,_) :: sign -> assert (id = id'); sign
-  | [] -> assert false
-
 let instance_from_named_context sign =
   let rec inst_rec = function
     | (id,None,_) :: sign -> mkVar id :: inst_rec sign
diff --git a/kernel/sign.mli b/kernel/sign.mli
index a35f61d229..6ba3e4fff7 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -20,7 +20,6 @@ type section_context = named_context
 
 val empty_named_context : named_context
 val add_named_decl : named_declaration -> named_context -> named_context
-val pop_named_decl : identifier -> named_context -> named_context
 
 val lookup_named : identifier -> named_context -> named_declaration
 val named_context_length : named_context -> int