diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 14:25:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-11 13:41:26 +0200 |
| commit | 81107b12644c78f204d0a46df520b8b2d8e72142 (patch) | |
| tree | 85b9575ade7ce2dffff6ee66a652706c82b34d2c /pretyping/cases.ml | |
| parent | c538b7fd555828d9fba9ea97503fac6c70377b76 (diff) | |
Deprecate Evarconv.e_conv,e_cumul
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 16244d8c0..84f0aba8c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -315,13 +315,15 @@ let try_find_ind env sigma typ realnames = IsInd (typ,ind,names) let inh_coerce_to_ind evdref env loc ty tyi = - let sigma = !evdref in + let orig = !evdref in let expected_typ = inductive_template evdref env loc tyi in (* Try to refine the type with inductive information coming from the constructor and renounce if not able to give more information *) (* devrait être indifférent d'exiger leq ou pas puisque pour un inductif cela doit être égal *) - if not (e_cumul env evdref expected_typ ty) then evdref := sigma + match cumul env !evdref expected_typ ty with + | Some sigma -> evdref := sigma + | None -> evdref := orig let binding_vars_of_inductive sigma = function | NotInd _ -> [] @@ -427,7 +429,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let current = if List.is_empty deps && isEvar !(pb.evdref) typ then (* Don't insert coercions if dependent; only solve evars *) - let _ = e_cumul pb.env pb.evdref indt typ in + let () = Option.iter ((:=) pb.evdref) (cumul pb.env !(pb.evdref) indt typ) in current else (evd_comb2 (Coercion.inh_conv_coerce_to true pb.env) @@ -1738,9 +1740,10 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = let evd,tt = Typing.type_of extenv !evdref t in evdref := evd; (t,tt) in - let b = e_cumul env evdref tt (mkSort s) (* side effect *) in - if not b then anomaly (Pp.str "Build_tycon: should be a type."); - { uj_val = t; uj_type = tt } + match cumul env !evdref tt (mkSort s) with + | None -> anomaly (Pp.str "Build_tycon: should be a type."); + | Some sigma -> evdref := sigma; + { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return |