+ let patterns_of pl =
+ let constructors, leftno =
+ let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in
+ let _,_,_,cl = List.nth tys n in
+ cl,leftno
+ in
+ let rec eat_branch n ty context ctx pat =
+ match (ty, pat) with
+ | TSkip t,_
+ | Forall (_,_,t),_
+ | Arrow (_, t), _ when n > 0 ->
+ eat_branch (pred n) t context ctx pat
+ | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*)
+ (*CSC: unify the three cases below? *)
+ | Arrow (_, t), NCic.Lambda (name, ty, t') ->
+ let ctx =
+ (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
+ let ctx =
+ (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | TSkip t,NCic.Lambda (name, ty, t') ->
+ let ctx = None::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | Top,_ -> assert false (* IMPOSSIBLE *)
+ | TSkip _, _
+ | Forall _,_
+ | Arrow _,_ -> assert false (*BUG here, eta-expand!*)
+ | _, _ -> context,ctx, pat
+ in
+ try
+ List.map2
+ (fun (_, _name, ty) pat ->
+ (*BUG: recomputing every time the type of the constructor*)
+ let ty = typ_of status ~metasenv context ty in
+ let context,lhs,rhs = eat_branch leftno ty context [] pat in
+ let rhs =
+ (* UnsafeCoerce not always required *)
+ UnsafeCoerce (term_of status ~metasenv context rhs)
+ in
+ lhs,rhs
+ ) constructors pl
+ with Invalid_argument _ -> assert false
+ in
+ (match classify_not_term status [] (NCic.Const ref) with
+ | `PropKind
+ | `KindOrType
+ | `Kind -> assert false (* IMPOSSIBLE *)
+ | `Proposition ->
+ (match patterns_of pl with
+ [] -> BottomElim
+ | [lhs,rhs] -> fomega_lift_term (- List.length lhs) rhs
+ | _ -> assert false)
+ | `Type ->
+ Match (ref,term_of status ~metasenv context t, patterns_of pl))