1 files changed, 0 insertions, 147 deletions
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
deleted file mode 100644
index 0191b6391..000000000
--- a/kernel/instantiate.ml
+++ /dev/null
@@ -1,147 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Term
-open Sign
-open Evd
-open Declarations
-open Environ
-
-let is_id_inst inst =
-  let is_id (id,c) = match kind_of_term c with
-    | IsVar id' -> id = id'
-    | _ -> false
-  in
-  List.for_all is_id inst
-
-let instantiate sign c args =
-  let inst = instantiate_named_context sign args in
-  if is_id_inst inst then
-    c
-  else
-    replace_vars inst c
-
-(* Vérifier que les instances des let-in sont compatibles ?? *)
-let instantiate_sign_including_let sign args =
-  let rec instrec = function
-    | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
-    | ([],[])                        -> []
-    | ([],_) | (_,[]) ->
-    anomaly "Signature and its instance do not match"
-  in 
-  instrec (sign,args)
-
-let instantiate_evar sign c args =
-  let inst = instantiate_sign_including_let sign args in
-  if is_id_inst inst then
-    c
-  else
-    replace_vars inst c
-
-let instantiate_constr sign c args =
-  let sign = List.map (fun (sp,b,t) -> (basename sp,b,t)) sign in
-  instantiate sign c args
-
-let instantiate_type sign tty args =
-  type_app (fun c -> instantiate_constr sign c args) tty
-
-(* Constants. *)
-
-(* constant_type gives the type of a constant *)
-let constant_type env sigma sp =
-  let cb = lookup_constant sp env in
-  cb.const_type  
-
-type const_evaluation_result = NoBody | Opaque
-
-exception NotEvaluableConst of const_evaluation_result
-
-let constant_value env sp =
-  let cb = lookup_constant sp env in
-  if cb.const_opaque then raise (NotEvaluableConst Opaque);
-  match cb.const_body with
-    | Some body -> body
-    | None -> raise (NotEvaluableConst NoBody)
-
-let constant_opt_value env cst =
-  try Some (constant_value env cst)
-  with NotEvaluableConst _ -> None
-
-(* Existentials. *)
-
-let name_of_existential n = id_of_string ("?" ^ string_of_int n)
-
-let existential_type sigma (n,args) =
-  let info = Evd.map sigma n in
-  let hyps = info.evar_hyps in
-  (* TODO: check args [this comment was in Typeops] *)
-  instantiate_evar hyps info.evar_concl (Array.to_list args)
-
-exception NotInstantiatedEvar
-
-let existential_value sigma (n,args) =
-  let info = Evd.map sigma n in
-  let hyps = info.evar_hyps in
-  match evar_body info with
-    | Evar_defined c ->
-	instantiate_evar hyps c (Array.to_list args)
-    | Evar_empty ->
-	raise NotInstantiatedEvar
-
-let existential_opt_value sigma ev =
-  try Some (existential_value sigma ev)
-  with NotInstantiatedEvar -> None
-
-
-type evaluable_reference =
-  | EvalConst of constant
-  | EvalVar of identifier
-  | EvalRel of int
-  | EvalEvar of existential
-
-let mkEvalRef = function
-  | EvalConst cst -> mkConst cst
-  | EvalVar id -> mkVar id
-  | EvalRel n -> mkRel n
-  | EvalEvar ev -> mkEvar ev
-
-let isEvalRef c = match kind_of_term c with
-  | IsConst _ | IsVar _ | IsRel _ | IsEvar _ -> true
-  | _ -> false
-
-let destEvalRef c = match kind_of_term c with
-  | IsConst cst ->  EvalConst cst
-  | IsVar id  -> EvalVar id
-  | IsRel n -> EvalRel n
-  | IsEvar ev -> EvalEvar ev
-  | _ -> anomaly "Not an evaluable reference"
-
-let evaluable_reference sigma env = function
-  | EvalConst sp -> evaluable_constant env sp
-  | EvalVar id -> evaluable_named_decl env id
-  | EvalRel n -> evaluable_rel_decl env n
-  | EvalEvar (ev,_) -> Evd.is_defined sigma ev
-
-let reference_opt_value sigma env = function
-  | EvalConst cst -> constant_opt_value env cst
-  | EvalVar id -> lookup_named_value id env
-  | EvalRel n -> lookup_rel_value n env
-  | EvalEvar ev -> existential_opt_value sigma ev
-
-exception NotEvaluable
-let reference_value sigma env c =
-  match reference_opt_value sigma env c with
-    | None -> raise NotEvaluable
-    | Some d -> d
-
-