fact: Definition new_destruct {A : Type} (n : A) : tactic := \tactic g => '(m: nparams, nindx, (existT _ isort it), constrs) <- get_ind A; atele <- get_ind_atele it nparams nindx A; cts <- M.map (fun c_dyn : dyn => dcase c_dyn as dtype, delem in ty <- M.evar (stype_of isort); b <- M.cumul UniCoq ty dtype; if b then el <- M.evar ty; M.cumul_or_fail UniCoq el delem;; get_CTele it nparams nindx ty el else M.failwith "Couldn't unify the type of the inductive with the type of the constructor" ) constrs; cts <- apply_params_constrs nparams atele cts; let it := mprojT1 (apply_args it atele nparams) in let atele := mprojT2 (apply_args _ atele nparams) in gt <- M.goal_type g; rsG <- sort_goal gt; let (rsort, sG) := rsG in n' <- M.coerce n; rt <- abstract_goal sG atele n'; let sg := reduce RedSimpl (mmap ( fun ct => (selem_of (branch_of_CTele rt ct)) ) cts) in goals <- M.map (fun ty=> r <- M.evar ty; M.ret (Metavar Typeₛ _ r)) sg; branches <- M.map M.goal_to_dyn goals; let tsg := reduce RedHNF (type_of sg) in let rrf := reduce RedSimpl (RTele_Fun rt) in let rrt := reduce RedSimpl (RTele_Type rt) in let type := reduce RedHNF (type_of n') in caseterm <- M.makecase {| case_ind := type; case_val := n'; case_return := Dyn rrf; case_branches := branches |}; (let '(Metavar s _ ge) := g in M.unify_or_fail UniCoq caseterm (Dyn ge);; M.ret tt );; M.map (fun (g : goal gs_open) => match g with | (Metavar _ _ g) => M.ret (m: tt, (AnyMetavar _ _ g)) end ) goals.
imports: Mtac2(Logic Datatypes List Sorts Base MTeleMatch MFix) Mtac2.tactics(Tactics ImportedTactics) Strings.String Mtac2.lib.Specif