retire profile

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

2 files changed, 18 insertions, 1 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 18e3d2c32..21ab932eb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -840,12 +840,14 @@ let fconv cv_pb env sigma t1 t2 =
 let conv env = fconv CONV env
 let conv_leq env = fconv CONV_LEQ env 
 
+(*
 let convleqkey = Profile.declare_profile "conv_leq";;
 let conv_leq env sigma t1 t2 = Profile.profile4 convleqkey conv_leq env sigma t1 t2;;
 
 
 let convkey = Profile.declare_profile "conv";;
 let conv env sigma t1 t2 = Profile.profile4 convleqkey conv env sigma t1 t2;;
+*)
 
 let conv_forall2 f env sigma v1 v2 =
   array_fold_left2 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index da0266752..65be6547b 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -26,9 +26,11 @@ let assumption_of_judgment env sigma j =
     | IsSort s -> j.uj_val
     | _ -> error_assumption CCI env j.uj_val
 
+(*
 let aojkey = Profile.declare_profile "assumption_of_judgment";;
 let assumption_of_judgment env sigma j
   = Profile.profile3 aojkey assumption_of_judgment env sigma j;;
+*)
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env sigma j =
@@ -46,8 +48,10 @@ let relative env sigma n =
   with Not_found -> 
     error_unbound_rel CCI env sigma n
 
+(*
 let relativekey = Profile.declare_profile "relative";;
 let relative env sigma n = Profile.profile3 relativekey relative env sigma n;;
+*)
 
 (* Management of context of variables. *)
 
@@ -83,9 +87,11 @@ let check_hyps id env sigma hyps =
 
 let type_of_constant = Instantiate.constant_type
 
+(*
 let tockey = Profile.declare_profile "type_of_constant";;
 let type_of_constant env sigma c 
   = Profile.profile3 tockey type_of_constant env sigma c;;
+*)
 
 (* Inductive types. *)
 
@@ -93,9 +99,11 @@ let type_of_inductive env sigma i =
   (* TODO: check args *)
   mis_arity (lookup_mind_specif i env)
 
+(*
 let toikey = Profile.declare_profile "type_of_inductive";;
 let type_of_inductive env sigma i
   = Profile.profile3 toikey type_of_inductive env sigma i;;
+*)
 
 (* Constructors. *)
 
@@ -104,10 +112,11 @@ let type_of_constructor env sigma cstr =
     (index_of_constructor cstr) 
     (lookup_mind_specif (inductive_of_constructor cstr) env)
 
+(*
 let tockey = Profile.declare_profile "type_of_constructor";;
 let type_of_constructor env sigma cstr
   = Profile.profile3 tockey type_of_constructor env sigma cstr;;
-
+*)
 
 let type_of_existential env sigma ev =
   Instantiate.existential_type sigma ev
@@ -218,9 +227,11 @@ let type_of_case env sigma ci pj cj lfj =
   { uj_val  = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
     uj_type = rslty }
 
+(*
 let tocasekey = Profile.declare_profile "type_of_case";;
 let type_of_case env sigma ci pj cj lfj
   = Profile.profile6 tocasekey type_of_case env sigma ci pj cj lfj;;
+*)
 
 (* Prop and Set *)
 
@@ -337,9 +348,11 @@ let apply_rel_list env sigma nocheck argjl funj =
   in 
   apply_rec 1 (body_of_type funj.uj_type) Constraint.empty argjl
 
+(*
 let applykey = Profile.declare_profile "apply_rel_list";;
 let apply_rel_list env sigma nocheck argjl funj
   = Profile.profile5 applykey apply_rel_list env sigma nocheck argjl funj;;
+*)
 
 (* Fixpoints. *)
 
@@ -709,8 +722,10 @@ let check_fix env sigma ((nvect,bodynum),(types,names,bodies as recdef)) =
       error_ill_formed_rec_body	CCI env err (List.rev names) i bodies
   done 
 
+(*
 let cfkey = Profile.declare_profile "check_fix";;
 let check_fix env sigma fix = Profile.profile3 cfkey check_fix env sigma fix;;
+*)
 
 (* Co-fixpoints. *)