diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 67 |
1 files changed, 34 insertions, 33 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4962b89a0..9e024b1c2 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -28,6 +28,7 @@ open CErrors open Util open Names open Evd +open Constr open Term open Termops open Environ @@ -44,7 +45,6 @@ open Pretype_errors open Glob_term open Glob_ops open Evarconv -open Misctypes open Ltac_pretype module NamedDecl = Context.Named.Declaration @@ -117,7 +117,7 @@ open ExtraEnv exception Found of int array let nf_fix sigma (nas, cs, ts) = - let inj c = EConstr.to_constr sigma c in + let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in (nas, Array.map inj cs, Array.map inj ts) let search_guard ?loc env possible_indexes fixdefs = @@ -169,14 +169,6 @@ let _ = optread = is_strict_universe_declarations; optwrite = (:=) strict_universe_declarations }) -let _ = - Goptions.(declare_bool_option - { optdepr = false; - optname = "minimization to Set"; - optkey = ["Universe";"Minimization";"ToSet"]; - optread = Universes.is_set_minimization; - optwrite = (:=) Universes.set_minimization }) - (** Miscellaneous interpretation functions *) let interp_known_universe_level evd r = @@ -245,7 +237,7 @@ let interp_known_level_info ?loc evd = function with Not_found -> user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) -let interp_level_info ?loc evd : Misctypes.level_info -> _ = function +let interp_level_info ?loc evd : level_info -> _ = function | UUnknown -> new_univ_level_variable ?loc univ_rigid evd | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s @@ -315,7 +307,7 @@ let apply_inference_hook hook evdref frozen = match frozen with then try let sigma, c = hook sigma evk in - Evd.define evk (EConstr.Unsafe.to_constr c) sigma + Evd.define evk c sigma with Exit -> sigma else @@ -429,7 +421,7 @@ let ltac_interp_name_env k0 lvar env sigma = let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in let open Context.Rel.Declaration in - let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in + let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env else push_rel_context sigma ctxt' (pop_rel_context n env sigma) @@ -499,7 +491,7 @@ let interp_known_glob_level ?loc evd = function | GSet -> Univ.Level.set | GType s -> interp_known_level_info ?loc evd s -let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function +let interp_glob_level ?loc evd : glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set | GType s -> interp_level_info ?loc evd s @@ -532,7 +524,7 @@ let pretype_global ?loc rigid env evd gr us = interp_instance ?loc evd ~len l in let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in - (sigma, EConstr.of_constr c) + (sigma, c) let pretype_ref ?loc evdref env ref us = match ref with @@ -674,14 +666,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in let nbfix = Array.length lar in let names = Array.map (fun id -> Name id) names in - let _ = + let () = match tycon with | Some t -> let fixi = match fixkind with | GFix (vn,i) -> i | GCoFix i -> i - in e_conv env.ExtraEnv.env evdref ftys.(fixi) t - | None -> true + in + begin match conv env.ExtraEnv.env !evdref ftys.(fixi) t with + | None -> () + | Some sigma -> evdref := sigma + end + | None -> () in (* Note: bodies are not used by push_rec_types, so [||] is safe *) let newenv = push_rec_types !evdref (names,ftys,[||]) env in @@ -698,7 +694,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - Typing.check_type_fixpoint ?loc env.ExtraEnv.env evdref names ftys vdefj; + evdref := Typing.check_type_fixpoint ?loc env.ExtraEnv.env !evdref names ftys vdefj; let nf c = nf_evar !evdref c in let ftys = Array.map nf ftys in (** FIXME *) let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in @@ -793,9 +789,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match candargs with | [] -> [], j_val hj | arg :: args -> - if e_conv env.ExtraEnv.env evdref (j_val hj) arg then - args, nf_evar !evdref (j_val hj) - else [], j_val hj + begin match conv env.ExtraEnv.env !evdref (j_val hj) arg with + | Some sigma -> evdref := sigma; + args, nf_evar !evdref (j_val hj) + | None -> + [], j_val hj + end in let ujval = adjust_evar_source evdref na ujval in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in @@ -1082,9 +1081,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential !evdref cty || occur_existential !evdref tval) then - let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in - if b then (evdref := evd; cj, tval) - else + match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with + | Some evd -> (evdref := evd; cj, tval) + | None -> error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err ?loc (str "Cannot check cast with vm: " ++ @@ -1093,9 +1092,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in - if b then (evdref := evd; cj, tval) - else + match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with + | Some evd -> (evdref := evd; cj, tval) + | None -> error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end @@ -1109,7 +1108,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let f decl (subst,update) = let id = NamedDecl.get_id decl in - let t = replace_vars subst (EConstr.of_constr (NamedDecl.get_type decl)) in + let t = replace_vars subst (NamedDecl.get_type decl) in let c, update = try let c = List.assoc id update in @@ -1118,7 +1117,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t (lift n t') then mkRel n, update else raise Not_found with Not_found -> try let t' = env |> lookup_named id |> NamedDecl.get_type in @@ -1150,7 +1149,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D (* Correction of bug #5315 : we need to define an evar for *all* holes *) let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in let ev,_ = destEvar !evdref evkt in - evdref := Evd.define ev (to_constr !evdref v) !evdref; + evdref := Evd.define ev (nf_evar !evdref v) !evdref; (* End of correction of bug #5315 *) { utj_val = v; utj_type = s } @@ -1166,10 +1165,12 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D match valcon with | None -> tj | Some v -> - if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj - else + begin match cumul env.ExtraEnv.env !evdref v tj.utj_val with + | Some sigma -> evdref := sigma; tj + | None -> error_unexpected_type ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v + end let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env sigma in |