diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /proofs/tmp-src | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'proofs/tmp-src')
-rw-r--r-- | proofs/tmp-src | 56 |
1 files changed, 0 insertions, 56 deletions
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)) |