diff options
Diffstat (limited to 'plugins/subtac/subtac_pretyping_F.ml')
| -rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 36 |
1 files changed, 29 insertions, 7 deletions
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 16f2031b..7fcd4267 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: subtac_pretyping_F.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Util @@ -166,6 +166,28 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RProp c -> judge_of_prop_contents c | RType _ -> judge_of_new_Type () + let split_tycon_lam loc env evd tycon = + let rec real_split evd c = + let t = whd_betadeltaiota env evd c in + match kind_of_term t with + | Prod (na,dom,rng) -> evd, (na, dom, rng) + | Evar ev when not (Evd.is_defined_evar evd ev) -> + let (evd',prod) = define_evar_as_product evd ev in + let (_,dom,rng) = destProd prod in + evd',(Anonymous, dom, rng) + | _ -> error_not_product_loc loc env evd c + in + match tycon with + | None -> evd,(Anonymous,None,None) + | Some (abs, c) -> + (match abs with + | None -> + let evd', (n, dom, rng) = real_split evd c in + evd', (n, mk_tycon dom, mk_tycon rng) + | Some (init, cur) -> + evd, (Anonymous, None, Some (Some (init, succ cur), c))) + + (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [( evdref)] and *) (* the type constraint tycon *) @@ -233,7 +255,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let newenv = let marked_ftys = Array.map (fun ty -> let sort = Retyping.get_type_of env !evdref ty in - mkApp (Lazy.force Subtac_utils.fix_proto, [| sort; ty |])) + mkApp (delayed_force Subtac_utils.fix_proto, [| sort; ty |])) ftys in push_rec_types (names,marked_ftys,[||]) env @@ -355,7 +377,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct evd, Some ty') evdref tycon in - let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon_lam loc env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in let var = (name,None,j.utj_val) in @@ -586,11 +608,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype tycon env evdref lvar c).uj_val | IsType -> (pretype_type empty_valcon env evdref lvar c).utj_val in - evdref := fst (consider_remaining_unif_problems env !evdref); + evdref := consider_remaining_unif_problems env !evdref; if resolve_classes then - evdref := - Typeclasses.resolve_typeclasses ~onlyargs:false + (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:fail_evar env !evdref; + evdref := consider_remaining_unif_problems env !evdref); let c = if expand_evar then nf_evar !evdref c' else c' in if fail_evar then check_evars env Evd.empty !evdref c; c @@ -603,7 +625,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let understand_judgment sigma env c = let evdref = ref (create_evar_defs sigma) in let j = pretype empty_tycon env evdref ([],[]) c in - let evd,_ = consider_remaining_unif_problems env !evdref in + let evd = consider_remaining_unif_problems env !evdref in let j = j_nf_evar evd j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j |