C.Lambda (binder,source,(aux target (k+1)))
| _ ->
if (id = false_constr_id)
- then (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [])
- else (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/True.ind") 0 [])
+ then (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
+ else (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/True.ind"),0,[]))
in aux red_ty 1
)
constructor_list
let (proof',goals') =
EliminationTactics.elim_type_tac
- ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )
+ ~term:(C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
~status
in
(match goals' with