in
ProofEngineTypes.apply_tactic
(ReductionTactics.change_tac
- ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1'))
- (C.Appl [
- C.Lambda (
- C.Name "x", tty,
- C.MutCase (
- turi, typeno,
- (C.Lambda (
- (C.Name "x"),
+ ~pattern:(ProofEngineTypes.conclusion_pattern
+ (Some new_t1'))
+ (fun _ m u ->
+ C.Appl [ C.Lambda (C.Name "x", tty,
+ C.MutCase (turi, typeno,
+ (C.Lambda ((C.Name "x"),
(S.lift 1 tty),
(S.lift 2 tty'))),
(C.Rel 1), pattern
)
);
- t1]
- ))
+ t1], m, u))
status
))
~continuation:
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,[])))
+ (C.MutInd(LibraryObjects.false_URI (),0,[])))
status
in
(match goals' with
(T.then_
~start:
(ReductionTactics.change_tac
- ~pattern:(ProofEngineTypes.conclusion_pattern (Some gty'))
- (C.Appl [
+ ~pattern:(ProofEngineTypes.conclusion_pattern
+ (Some gty'))
+ (fun _ m u -> C.Appl [
C.Lambda (
C.Name "x", tty,
C.MutCase (
(C.Rel 1), pattern
)
);
- t2]
- )
- )
+ t2], m, u))
~continuation:
(
T.then_