diff options
| -rw-r--r-- | pretyping/cases.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 23 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/2966.v | 2 |
7 files changed, 23 insertions, 16 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 50396d854..3f1bead36 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1559,7 +1559,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = map_constr_with_full_binders push_binder aux x t | Evar ev -> let ty = get_type_of env sigma t in - let ty = Evarutil.evd_comb1 (refresh_universes false env) evdref ty in + let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let inst = List.map_i (fun i _ -> @@ -1577,7 +1577,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = let vl = List.map pi1 good in let ty = let ty = get_type_of env !evdref t in - Evarutil.evd_comb1 (refresh_universes false env) evdref ty + Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let ty = lift (-k) (aux x ty) in let depvl = free_rels ty in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 9522f9c24..13421bcde 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,7 +42,12 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -let refresh_universes ?(onlyalg=false) dir env evd t = +(** + forall A (l : list A) -> typeof A = Type i <= Datatypes.j -> i not refreshed + hd ?A (l : list t) -> A = t + +*) +let refresh_universes ?(onlyalg=false) pbty env evd t = let evdref = ref evd in let modified = ref false in let rec refresh dir t = @@ -88,7 +93,10 @@ let refresh_universes ?(onlyalg=false) dir env evd t = in aux 0 pos in let t' = - if isArity t then refresh dir t + if isArity t then + (match pbty with + | None -> t + | Some dir -> refresh dir t) else (refresh_term_evars false t; t) in if !modified then !evdref, t' else !evdref, t @@ -553,7 +561,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let id = next_name_away na avoid in let evd,t_in_sign = let s = Retyping.get_sort_of env evd t_in_env in - let evd,ty_t_in_sign = refresh_universes false env evd (mkSort s) in + let evd,ty_t_in_sign = refresh_universes (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd t_in_env ty_t_in_sign sign filter inst_in_env in let evd,b_in_sign = match b with @@ -572,7 +580,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = in let evd,ev2ty_in_sign = let s = Retyping.get_sort_of env evd ty_in_env in - let evd,ty_t_in_sign = refresh_universes false env evd (mkSort s) in + let evd,ty_t_in_sign = refresh_universes (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd ty_in_env ty_t_in_sign sign2 filter2 inst2_in_env in let evd,ev2_in_sign = @@ -1417,7 +1425,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = * context "hyps" and not referring to itself. *) -and evar_define conv_algo ?(choose=false) ?(dir=false) env evd pbty (evk,argsv as ev) rhs = +and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = match kind_of_term rhs with | Evar (evk2,argsv2 as ev2) -> if Evar.equal evk evk2 then @@ -1436,7 +1444,7 @@ and evar_define conv_algo ?(choose=false) ?(dir=false) env evd pbty (evk,argsv a (* so we recheck acyclicity *) if occur_evar evk body then raise (OccurCheckIn (evd',body)); (* needed only if an inferred type *) - let evd', body = refresh_universes dir env evd' body in + let evd', body = refresh_universes pbty env evd' body in (* Cannot strictly type instantiations since the unification algorithm * does not unify applications from left to right. * e.g problem f x == g y yields x==y and f==g (in that order) @@ -1520,8 +1528,7 @@ let reconsider_conv_pbs conv_algo evd = let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) = try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) - let dir = match pbty with Some d -> d | None -> false in - let evd = evar_define conv_algo ~choose ~dir env evd pbty ev1 t2 in + let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in reconsider_conv_pbs conv_algo evd with | NotInvertibleUsingOurAlgorithm t -> diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 6de8f5c8d..16a4aff5b 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -31,11 +31,11 @@ type conv_fun = type conv_fun_bool = env -> evar_map -> conv_pb -> constr -> constr -> bool -val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> +val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map val refresh_universes : ?onlyalg:bool (* Only algebraic universes *) -> - bool (* direction: true for levels lower than the existing levels *) -> + bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 27abdbade..6d7403031 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -595,7 +595,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = refreshed right away. *) let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in - let c = evd_comb1 (Evarsolve.refresh_universes true env) evdref c in + let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in let t = Retyping.get_type_of env !evdref c in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 1c41a5bb3..92bdd35ec 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes ~onlyalg:true false env !evdref j.uj_type + Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type else !evdref, j.uj_type let solve_evars env evdref c = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 300eb6dc6..219d03b9e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -936,7 +936,7 @@ let w_coerce env evd mv c = w_coerce_to_type env evd c cty mvty let unify_to_type env sigma flags c status u = - let sigma, c = refresh_universes false env sigma c in + let sigma, c = refresh_universes (Some false) env sigma c in let t = get_type_of env sigma (nf_meta sigma c) in let t = nf_betaiota sigma (nf_meta sigma t) in unify_0 env sigma CUMUL flags t u diff --git a/test-suite/bugs/closed/2966.v b/test-suite/bugs/closed/2966.v index e1c8d0047..debada853 100644 --- a/test-suite/bugs/closed/2966.v +++ b/test-suite/bugs/closed/2966.v @@ -7,7 +7,7 @@ Set Asymmetric Patterns. Module MemSig. Definition t: Type := list Type. - Definition Nth (sig: t) (n: nat): Type := + Definition Nth (sig: t) (n: nat) := nth n sig unit. End MemSig. |