diff options
| -rw-r--r-- | pretyping/pretyping.ml | 11 | ||||
| -rw-r--r-- | test-suite/success/Cases.v | 9 | ||||
| -rw-r--r-- | test-suite/success/TestRefine.v | 9 | ||||
| -rw-r--r-- | toplevel/command.ml | 13 |
4 files changed, 22 insertions, 20 deletions
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 diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 499c066064..ccd92f6960 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -31,10 +31,11 @@ Type (* Interaction with coercions *) Parameter bool2nat : bool -> nat. Coercion bool2nat : bool >-> nat. -Check (fun x => match x with - | O => true - | S _ => 0 - end:nat). +Definition foo : nat -> nat := + fun x => match x with + | O => true + | S _ => 0 + end. (****************************************************************************) (* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 82c5cf2e74..dd84402dfa 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -9,13 +9,11 @@ (************************************************************************) Lemma essai : forall x : nat, x = x. - refine ((fun x0 : nat => match x0 with | O => _ | S p => _ - end) - :forall x : nat, x = x). (* x0=x0 et x0=x0 *) + end)). Restart. @@ -145,11 +143,10 @@ Lemma essai : forall n : nat, {x : nat | x = S n}. Restart. refine - ((fun n : nat => match n with + (fun n : nat => match n with | O => _ | S p => _ - end) - :forall n : nat, {x : nat | x = S n}). + end). Restart. diff --git a/toplevel/command.ml b/toplevel/command.ml index 5d144f1961..5cccc225cd 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -113,11 +113,14 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = const_entry_opaque = opacity; const_entry_boxed = boxed } | Some comtyp -> - (* We use a cast to avoid troubles with evars in comtyp *) - (* that can only be resolved knowing com *) - let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv (DEFAULTcast,comtyp))) bl in - let b, imps = interp_constr_evars_impls env b in - let (body,typ) = destSubCast b in + let ty = generalize_constr_expr comtyp bl in + let b = abstract_constr_expr com bl in + let evdref = ref (Evd.create_evar_defs Evd.empty) in + let ty, impls = interp_type_evars_impls ~evdref env ty in + let b, imps = interp_casted_constr_evars_impls ~evdref env b ty in + let body, typ = nf_isevar !evdref b, nf_isevar !evdref ty in + check_evars env Evd.empty !evdref body; + check_evars env Evd.empty !evdref typ; imps, { const_entry_body = body; const_entry_type = Some typ; |