From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 proofs/tmp-src | 56 --------------------------------------------------------
 1 file changed, 56 deletions(-)
 delete mode 100644 proofs/tmp-src

(limited to 'proofs/tmp-src')

diff --git a/proofs/tmp-src b/proofs/tmp-src
deleted file mode 100644
index 1da11fe0..00000000
--- 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))
-- 
cgit v1.2.3