From 12a13c739a71cb4e796cc9e6e1596bb75be4ff1c Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 7 Nov 2008 18:22:08 +0000 Subject: Slight change of the semantics of user-given casts: they don't really help the type _checking_ anymore (they don't become typing constraints) but they permit to coerce a subterm in a type. In particular, when using a VM cast we avoid unneeded, unexpected conversions using the default machine (oops!). Also remove the corresponding comment in pretyping and fix the wrong use of casts in toplevel/command: accept the trouble of using evars. This has the somewhat adverse effect that when typing casted object we now have no typing constraints (see e.g. examples in Cases.v)! Probably, this will be backtracked partially tomorrow as many contribs can rely on it and the change could make some unifications fail (in particular with deep coercions). Let's try anyway! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11558 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pretyping.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7400cdd9ce..2921cd5365 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -558,7 +558,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar (evars_of !evdref) pred in let p = nf_evar (evars_of !evdref) p in - (* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*) let f cs b = let n = rel_context_length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) @@ -575,7 +574,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct cs.cs_args in let env_c = push_rels csgn env in -(* msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *) let bj = pretype (mk_tycon pi) env_c evdref lvar b in it_mkLambda_or_LetIn bj.uj_val cs.cs_args in let b1 = f cstrs.(0) b1 in @@ -600,9 +598,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj | CastConv (k,t) -> let tj = pretype_type empty_valcon env evdref lvar t in - let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in - (* User Casts are for helping pretyping, experimentally not to be kept*) - (* ... except for Correctness *) + let cj = pretype empty_tycon env evdref lvar c in + let cj = match k with + | VMcast when not (occur_existential cj.uj_type || occur_existential tj.utj_val) -> + ignore (Reduction.vm_conv Reduction.CUMUL env cj.uj_type tj.utj_val); cj + | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tj.utj_val) + in let v = mkCast (cj.uj_val, k, tj.utj_val) in { uj_val = v; uj_type = tj.utj_val } in inh_conv_coerce_to_tycon loc env evdref cj tycon -- cgit v1.2.3