diff options
| author | Pierre-Marie Pédrot | 2015-02-11 17:55:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-11 17:55:50 +0100 |
| commit | 37076a63ebd1491f26a6c5a3d67e054c106589b3 (patch) | |
| tree | 702d4be5c21408ce819b1265ac7cd4d5d2c2866d /pretyping | |
| parent | 956b7c4304582b1e9e3ca0bb34944bcbac18c0cc (diff) | |
| parent | ac65eef8bbc2e405f1964f35c6a129dfa1755888 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 6 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fdb19d3780..7c3165fa8e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1644,7 +1644,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = in aux (0,extenv,subst0) t0 -let build_tycon loc env tycon_env subst tycon extenv evdref t = +let build_tycon loc env tycon_env s subst tycon extenv evdref t = let t,tt = match t with | None -> (* This is the situation we are building a return predicate and @@ -1659,6 +1659,8 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t = let evd,tt = Typing.e_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 } (* For a multiple pattern-matching problem Xi on t1..tn with return @@ -1780,7 +1782,7 @@ let build_inversion_problem loc env sigma tms t = mat = [eqn1;eqn2]; caseloc = loc; casestyle = RegularStyle; - typing_function = build_tycon loc env pb_env subst} in + typing_function = build_tycon loc env pb_env s subst} in let pred = (compile pb).uj_val in (!evdref,pred) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index a6e2bc19db..cf6ac619dd 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -441,7 +441,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = try let term = Retyping.expand_projection env sigma p c' [] in aux env term mk_ctx next - with Retyping.RetypeError _ -> raise PatternMatchingFailure + with Retyping.RetypeError _ -> next () else try_aux [env] [c'] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next |