summaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml33
1 files changed, 24 insertions, 9 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fdb19d37..fcbe90b6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -285,11 +285,13 @@ let inductive_template evdref env tmloc ind =
applist (mkIndU indu,List.rev evarl)
let try_find_ind env sigma typ realnames =
- let (IndType(_,realargs) as ind) = find_rectype env sigma typ in
+ let (IndType(indf,realargs) as ind) = find_rectype env sigma typ in
let names =
match realnames with
| Some names -> names
- | None -> List.make (List.length realargs) Anonymous in
+ | None ->
+ let ind = fst (fst (dest_ind_family indf)) in
+ List.make (inductive_nrealdecls ind) Anonymous in
IsInd (typ,ind,names)
let inh_coerce_to_ind evdref env loc ty tyi =
@@ -730,7 +732,17 @@ let set_declaration_name x (_,c,t) = (x,c,t)
let recover_initial_subpattern_names = List.map2 set_declaration_name
-let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t))
+let recover_and_adjust_alias_names names sign =
+ let rec aux = function
+ | [],[] ->
+ []
+ | x::names, (_,None,t)::sign ->
+ (x,(alias_of_pat x,None,t)) :: aux (names,sign)
+ | names, (na,(Some _ as c),t)::sign ->
+ (PatVar (Loc.ghost,na),(na,c,t)) :: aux (names,sign)
+ | _ -> assert false
+ in
+ List.split (aux (names,sign))
let push_rels_eqn sign eqn =
{eqn with
@@ -1644,7 +1656,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 +1671,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
@@ -1693,11 +1707,12 @@ let build_inversion_problem loc env sigma tms t =
let pat,acc = make_patvar t acc in
let indf' = lift_inductive_family n indf in
let sign = make_arity_signature env true indf' in
- let sign = recover_alias_names alias_of_pat (pat :: List.rev patl) sign in
- let p = List.length realargs in
+ let patl = pat :: List.rev patl in
+ let patl,sign = recover_and_adjust_alias_names patl sign in
+ let p = List.length patl in
let env' = push_rel_context sign env in
- let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in
- patl@pat::patl',acc_sign,acc
+ let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
+ List.rev_append patl patl',acc_sign,acc
| (t, NotInd (bo,typ)) :: tms ->
let pat,acc = make_patvar t acc in
let d = (alias_of_pat pat,None,typ) in
@@ -1780,7 +1795,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)