diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 11 | ||||
| -rw-r--r-- | pretyping/cases.mli | 5 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 41 |
3 files changed, 32 insertions, 25 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aa24733d9f..27c1dd0316 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1934,14 +1934,19 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = *) let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = + let refresh_tycon sigma t = + refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true) + env sigma t + in let preds = match pred, tycon with (* No return clause *) | None, Some t when not (noccur_with_meta 0 max_int t) -> (* If the tycon is not closed w.r.t real variables, we try *) (* two different strategies *) - (* First strategy: we abstract the tycon wrt to the dependencies *) - let p1 = + (* First strategy: we abstract the tycon wrt to the dependencies *) + let sigma, t = refresh_tycon sigma t in + let p1 = prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in (* Second strategy: we build an "inversion" predicate *) let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in @@ -1952,7 +1957,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = (* No dependent type constraint, or no constraints at all: *) (* we use two strategies *) let sigma,t = match tycon with - | Some t -> sigma,t + | Some t -> refresh_tycon sigma t | None -> let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma ((t, _), sigma, _) = diff --git a/pretyping/cases.mli b/pretyping/cases.mli index ba566f3744..ee4148de64 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -114,10 +114,11 @@ val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment val prepare_predicate : Loc.t -> (Evarutil.type_constraint -> - Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) -> + Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) -> Environ.env -> Evd.evar_map -> (Term.types * tomatch_type) list -> Context.Rel.t list -> Constr.constr option -> - 'a option -> (Evd.evar_map * Names.name list * Term.constr) list + glob_constr option -> + (Evd.evar_map * Names.name list * Term.constr) list diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f0aa9b564f..02e10d7fc1 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,33 +42,34 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -let refresh_level evd s = - match Evd.is_sort_variable evd s with - | None -> true - | Some l -> not (Evd.is_flexible_level evd l) - let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) pbty env evd t = let evdref = ref evd in let modified = ref false in - let rec refresh status dir t = - match kind_of_term t with - | Sort (Type u as s) when - (match Univ.universe_level u with - | None -> true - | Some l -> not onlyalg && refresh_level evd s) -> + let refresh_sort status dir s = let s' = evd_comb0 (new_sort_variable status) evdref in let evd = if dir then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' in - modified := true; evdref := evd; mkSort s' + modified := true; evdref := evd; mkSort s' + in + let rec refresh onlyalg status dir t = + match kind_of_term t with + | Sort (Type u as s) -> + (match Univ.universe_level u with + | None -> refresh_sort status dir s + | Some l -> + (match Evd.universe_rigidity evd l with + | UnivRigid -> if not onlyalg then refresh_sort status dir s else t + | UnivFlexible alg -> + if onlyalg && alg then + (evdref := Evd.make_flexible_variable !evdref false l; t) + else t)) | Sort (Prop Pos as s) when refreshset && not dir -> - let s' = evd_comb0 (new_sort_variable status) evdref in - let evd = set_leq_sort env !evdref s s' in - modified := true; evdref := evd; mkSort s' + refresh_sort status dir s | Prod (na,u,v) -> - mkProd (na,u,refresh status dir v) + mkProd (na, u, refresh onlyalg status dir v) | _ -> t (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars top t = @@ -81,7 +82,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh univ_flexible true evi.evar_concl in + let ty' = refresh onlyalg univ_flexible true evi.evar_concl in if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () @@ -101,9 +102,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) in let t' = if isArity t then - (match pbty with - | None -> t - | Some dir -> refresh status dir t) + match pbty with + | None -> refresh true univ_flexible false t + | Some dir -> refresh onlyalg status dir t else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t |