- PET.apply_tactic tactic status
- in
- PET.mk_tactic lazy_destruct
-
-(* destruct performs either injection or discriminate *)
-(* equivalent to Coq's "analyze equality" *)
-let destruct_tac = function
- | Some term -> destruct ~first_time:true term
- | None ->
- let destruct_all status =
- let (proof, goal) = status in
- let _,metasenv,_subst,_,_, _ = proof in
- let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let mk_lterm term c m ug =
- let distance = List.length c - List.length context in
- S.lift distance term, m, ug
- in
- let rec mk_tactics first_time i tacs = function
- | [] -> List.rev tacs
- | Some _ :: tl ->
- let lterm = mk_lterm (C.Rel i) in
- let tacs = lazy_destruct_tac ~first_time ~lterm :: tacs in
- mk_tactics false (succ i) tacs tl
- | _ :: tl -> mk_tactics first_time (succ i) tacs tl
- in
- let tactics = mk_tactics false 1 [] context in
- PET.apply_tactic (T.seq ~tactics) status
+ let tactics = match xterms with
+ | Some terms ->
+ let map term = destruct ~first_time:false (mk_lterm term) in
+ List.map map terms
+ | None ->
+ let rec mk_tactics first_time i tacs = function
+ | [] -> List.rev tacs
+ | Some _ :: tl ->
+ let lterm = mk_lterm (C.Rel i) in
+ let tacs = destruct ~first_time lterm :: tacs in
+ mk_tactics false (succ i) tacs tl
+ | _ :: tl -> mk_tactics first_time (succ i) tacs tl
+ in
+ mk_tactics false 1 [] context