fact: Definition get_ind_cts (A : Type) (offset : nat) : M (nat * {s : Sort & { it : ITele s & mlist (NDCTele it)}}) := '(m: nparams, nindx, (existT _ isort it), constrs) <- get_ind A; let constrs := mskipn offset constrs in atele <- get_ind_atele it nparams nindx A; cts <- M.map (fun c_dyn : dyn => dcase c_dyn as dtype, delem in let ty_c := reduce (RedWhd RedAll) (S.stype_of isort) in ty <- M.evar ty_c; b <- M.cumul UniMatchNoRed ty dtype; if b then let el_c := reduce (RedWhd RedAll) (S.selem_of ty) in el <- M.evar el_c; M.cumul UniMatchNoRed el delem;; get_NDCTele it nindx ty el else M.failwith "Couldn't unify the type of the inductive with the type of the constructor" ) constrs; M.ret (nindx, existT _ _ (existT _ _ cts)).
imports: Coq.Strings.String Mtac2(Base Logic Datatypes List Sorts DepDestruct MTeleMatch)