resolution du pb d'efficacite du a Sign.add_named_decl

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

5 files changed, 31 insertions, 32 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7113b4040e..e4fc5c0e9d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -61,11 +61,10 @@ let evaluable_rel n env =
   with Not_found -> 
     false
 
-let rel_context_app f env =
+let push_rel d env =
   { env with
-      env_rel_context = f env.env_rel_context }
+      env_rel_context = add_rel_decl d env.env_rel_context }
 
-let push_rel d   = rel_context_app (add_rel_decl d)
 let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
 let push_rec_types (lna,typarray,_) env =
   let ctxt =
@@ -96,11 +95,9 @@ let evaluable_named id env =
   with Not_found -> 
     false
 
-let named_context_app f env =
+let push_named d env =
   { env with
-      env_named_context = f env.env_named_context }
-
-let push_named d   = named_context_app (Sign.add_named_decl d)
+      env_named_context = Sign.add_named_decl d env.env_named_context }
 
 let reset_context env =
   { env with
@@ -125,10 +122,6 @@ let lookup_constant sp env =
   Spmap.find sp env.env_globals.env_constants
 
 let add_constant sp cb env =
-  let _ =
-    try
-      let _ = lookup_constant sp env in failwith "already declared constant"
-    with Not_found -> () in
   let new_constants = Spmap.add sp cb env.env_globals.env_constants in
   let new_locals = (Constant,sp)::env.env_globals.env_locals in
   let new_globals = 
@@ -167,10 +160,6 @@ let lookup_mind sp env =
   Spmap.find sp env.env_globals.env_inductives
 
 let add_mind sp mib env =
-  let _ =
-    try 
-      let _ = lookup_mind sp env in failwith "already defined inductive"
-    with Not_found -> () in
   let new_inds = Spmap.add sp mib env.env_globals.env_inductives in
   let new_locals = (Inductive,sp)::env.env_globals.env_locals in
   let new_globals = 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ad36e2941b..f424f79dbf 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -54,7 +54,20 @@ let push_rel_or_named_def push (id,b,topt) env =
   let env'' = push (id,Some j.uj_val,typ) env' in
   (cst,env'')
 
-let push_named_def = push_rel_or_named_def push_named
+
+(* Same as push_named, but check that the variable is not already
+   there. Should *not* be done in Environ because tactics add temporary
+   hypothesis many many times, and the check performed here would
+   cost too much. *)
+let safe_push_named (id,_,_ as d) env =
+  let _ =
+    try
+      let _ = lookup_named id env in 
+      error ("identifier "^string_of_id id^" already defined")
+    with Not_found -> () in
+  push_named d env
+
+let push_named_def = push_rel_or_named_def safe_push_named
 let push_rel_def = push_rel_or_named_def push_rel
 
 let push_rel_or_named_assum push (id,t) env =
@@ -112,11 +125,21 @@ let add_global_declaration sp env (body,typ,cst,op) =
 (*s Global and local constant declaration. *)
 
 let add_constant sp ce env =
+  let _ =
+    try
+      let _ = lookup_constant sp env in
+      error ("constant "^string_of_path sp^" already declared")
+    with Not_found -> () in
   add_global_declaration sp env (safe_infer_declaration env ce)
 
 (* Insertion of inductive types. *)
 
 let add_mind sp mie env =
+  let _ =
+    try 
+      let _ = lookup_mind sp env in
+      error ("inductive "^string_of_path sp^" already declared")
+    with Not_found -> () in
   let mib = check_inductive env mie in
   let cst = mib.mind_constraints in
   Environ.add_mind sp mib (add_constraints cst env)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 071a67224a..10357f407c 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -45,11 +45,11 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 val add_constant : 
-  section_path -> global_declaration -> safe_environment -> safe_environment
+  constant -> global_declaration -> safe_environment -> safe_environment
 
 (* Adding an inductive type *)
 val add_mind : 
-  section_path -> Indtypes.mutual_inductive_entry -> safe_environment ->
+  mutual_inductive -> Indtypes.mutual_inductive_entry -> safe_environment ->
     safe_environment
 
 (* Adding universe constraints *)
diff --git a/kernel/sign.ml b/kernel/sign.ml
index da6ec5a11d..f0c275fa37 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -19,19 +19,13 @@ type named_context = named_declaration list
 
 let empty_named_context = []
 
+let add_named_decl d sign = d::sign
 
 let rec lookup_named id = function
   | (id',_,_ as decl) :: _ when id=id' -> decl
   | _ :: sign -> lookup_named id sign
   | [] -> raise Not_found
 
-  
-let add_named_decl (id,_,_ as d) sign =
-  try
-    let _ = lookup_named id sign in 
-    failwith ("identifier "^string_of_id id^" already defined")
-  with _ -> d::sign
-
 let named_context_length = List.length
 
 let instance_from_named_context sign =
@@ -99,10 +93,6 @@ let push_named_to_rel_context hyps ctxt =
 (*       Term constructors       *)
 (*********************************)
 
-let it_mkNamedProd_or_LetIn   =
-  List.fold_left (fun c d -> mkNamedProd_or_LetIn d c)
-let it_mkNamedLambda_or_LetIn =
-  List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
 let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
 let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 6ba3e4fff7..e5de5613d8 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -58,9 +58,6 @@ val fold_rel_context_reverse :
 
 (*s Term constructors *)
 
-val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
-val it_mkNamedProd_or_LetIn : types -> named_context -> types
-
 val it_mkLambda_or_LetIn : constr -> rel_context -> constr
 val it_mkProd_or_LetIn : types -> rel_context -> types