let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
(match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with (* an equality *)
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
~start:
(fun ~status:((proof,goal) as status) ->
let _,metasenv,_,_ = proof in
- let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,gty = CicUtil.lookup_meta goal metasenv in
prerr_endline ("XXXX goal " ^ string_of_int goal) ;
prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ;
prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ;
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
(match goals' with
[goal'] ->
let _,metasenv',_,_ = proof' in
- let _,context',gty' = List.find (function (m,_,_) -> m=goal') metasenv' in
-prerr_endline ("XXXX gty " ^ CicPp.ppterm gty') ;
-prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ;
-prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ;
-prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ;
-ignore (List.map (fun t -> prerr_endline ("XXXX t " ^ CicPp.ppterm t)) pattern) ;
-prerr_endline ("XXXX case " ^ CicPp.ppterm (C.Appl [
- C.Lambda (
- C.Name "x", tty,
- C.MutCase (
- turi, typeno,
- (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))),
- (C.Rel 1), pattern
- )
- ); t2])) ;
+ let _,context',gty' =
+ CicUtil.lookup_meta goal' metasenv'
+ in
T.then_
~start:
(P.change_tac
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,gty = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with
(C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
(match goals' with
[goal'] ->
let _,metasenv',_,_ = proof' in
- let _,context',gty' = List.find (function (m,_,_) -> m=goal') metasenv' in
-prerr_endline ("XXXX gty " ^ CicPp.ppterm gty') ;
-prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ;
-prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ;
-prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ;
-ignore (List.map (fun t -> prerr_endline ("XXXX t " ^ CicPp.ppterm t)) pattern) ;
-prerr_endline ("XXXX case " ^ CicPp.ppterm (C.Appl [
- C.Lambda (
- C.Name "x", tty,
- C.MutCase (
- turi, typeno,
- (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))),
- (C.Rel 1), pattern
- )
- ); t2'])) ;
+ let _,context',gty' =
+ CicUtil.lookup_meta goal' metasenv'
+ in
T.then_
~start:
(P.change_tac