C.Lambda (binder,source,(aux target (k+1)))
| _ ->
if (id = false_constr_id)
- then (C.MutInd(LibraryObjects.false_URI,0,[]))
- else (C.MutInd(LibraryObjects.true_URI,0,[]))
+ then (C.MutInd(LibraryObjects.false_URI (),0,[]))
+ else (C.MutInd(LibraryObjects.true_URI (),0,[]))
in aux red_ty 1
)
constructor_list
let (proof',goals') =
ProofEngineTypes.apply_tactic
(EliminationTactics.elim_type_tac
- ~term:(C.MutInd(LibraryObjects.false_URI,0,[])))
+ ~term:(C.MutInd(LibraryObjects.false_URI (),0,[])))
status
in
(match goals' with