1 files changed, 56 insertions, 0 deletions
diff --git a/proofs/tmp-src b/proofs/tmp-src
new file mode 100644
index 00000000..1da11fe0
--- /dev/null
+++ b/proofs/tmp-src
@@ -0,0 +1,56 @@
+
+(********* 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))