]
;;
-let apply_tac (s,n,t) = exact_tac (s,n,Ast.Appl [t; Ast.Implicit `Vector]);;
+let apply_tac (s,n,t) =
+ let t = Ast.Appl [t; Ast.Implicit `Vector] in
+ exact_tac (s,n,t)
+;;
type indtyinfo = {
rightno: int;
}
;;
-let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
+let analyze_indty_tac ~what indtyref =
+ distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let status, what = disambiguate status what None (ctx_of goalty) in
let status, ty_what = typeof status (ctx_of what) what in
exec id_tac status goal)
;;
-let elim_tac ~what ~where =
+let elim_tac ~what:(txt,len,what) ~where =
+ let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
let indtyinfo = ref None in
let sort = ref None in
let compute_goal_sort_tac = distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let status, goalsort = typeof status (ctx_of goalty) goalty in
+ let goalsort = fix_sorts goalsort in
sort := Some goalsort;
exec id_tac status goal)
in
"_rect_" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] sort
| _ -> assert false
in
- let holes =
- HExtlib.mk_list (Ast.Implicit `JustOne)
- (ity.leftno+1+ ity.consno + ity.rightno) in
let eliminator =
let _,_,w = what in
- Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
+ Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
in
exact_tac ("",0,eliminator) status) ])
;;
| _ -> assert false
in
let name =
- match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq" ^ suffix
+ match dir with
+ `LeftToRight -> "eq" ^ suffix ^ "_r"
+ | `RightToLeft -> "eq" ^ suffix
in
block_tac
[ select_tac ~where ~job:(`Substexpand 1) true;
instantiate status goal t
;;
-let cases_tac ~what ~where =
+let cases_tac ~what:(txt,len,what) ~where =
+ let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
let indtyinfo = ref None in
atomic_tac
(block_tac [