Remove old file (1999)

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

1 files changed, 0 insertions, 56 deletions

diff --git a/proofs/tmp-src b/proofs/tmp-src
deleted file mode 100644
index 1da11fe01d..0000000000
--- a/proofs/tmp-src
+++ /dev/null
@@ -1,56 +0,0 @@
-
-(********* INSTANTIATE ****************************************************)
-
-(* existential_type gives the type of an existential *)
-let existential_type env k = 
-  let (sp,args) = destConst k in
-  let evd = Evd.map (evar_map env) sp in
-  instantiate_constr 
-    (ids_of_sign evd.evar_hyps) evd.evar_concl.body (Array.to_list args)
-
-(* existential_value gives the value of a defined existential *)
-let existential_value env k =
-  let (sp,args) = destConst k in
-  if defined_const env k then
-    let evd = Evd.map (evar_map env) sp in
-    match evd.evar_body with
-      | EVAR_DEFINED c ->
- 	  instantiate_constr (ids_of_sign evd.evar_hyps) c (Array.to_list args)
-      | _ -> anomalylabstrm "termenv__existential_value"
-            [< 'sTR"The existential variable code just registered a" ;
-               'sPC ; 'sTR"grave internal error." >]
-  else 
-    failwith "undefined existential"
-
-
-(******* REDUCTION ********************************************************)
-
-
-(************ REDUCTION.MLI **********************************************)
-
-(*********** TYPEOPS *****************************************************)
-
-
-(* Constants or existentials. *)
-
-let type_of_constant_or_existential env c =
-  if is_existential c then
-    type_of_existential env c
-  else
-    type_of_constant env c
-
-
-(******** TYPING **********************************************************)
-
-    | IsMeta n ->
-       	let metaty =
-          try lookup_meta n env
-          with Not_found -> error "A variable remains non instanciated" 
-	in
-        (match kind_of_term metaty with
-           | IsCast (typ,kind) -> 
-	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, cst0)
-           | _ ->
-	       let (jty,cst) = execute mf env metaty in
-	       let k = whd_betadeltaiotaeta env jty.uj_type in
-	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, cst))