Bug fixed: analysing inductive type that contains implicit used to
duplicate the metas in the metasenv since the term was disambiguated
twice, in the analyze and in the tactic that uses the analyze.
lefts: NCic.term list;
rights: NCic.term list;
reference: NReference.reference;
lefts: NCic.term list;
rights: NCic.term list;
reference: NReference.reference;
let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
let leftno = List.length lefts in
let rightno = List.length rights in
let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
let leftno = List.length lefts in
let rightno = List.length rights in
+ let status,what = term_of_cic_term status what (ctx_of goalty) in
indtyref := Some {
rightno = rightno; leftno = leftno; consno = consno;
indtyref := Some {
rightno = rightno; leftno = leftno; consno = consno;
- lefts = lefts; rights = rights; reference = r;
+ lefts = lefts; rights = rights; reference = r; term = what
};
exec id_tac status goal)
;;
};
exec id_tac status goal)
;;
(match !sort with NCic.Sort x -> x | _ -> assert false))
in
let eliminator =
(match !sort with NCic.Sort x -> x | _ -> assert false))
in
let eliminator =
- let _,_,w = what in
- Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+ let what = (HExtlib.unopt !indtyinfo).term in
+ Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ]
in
exact_tac ("",0,eliminator) status) ])
;;
in
exact_tac ("",0,eliminator) status) ])
;;
atomic_tac
(block_tac [
analyze_indty_tac ~what indtyinfo;
atomic_tac
(block_tac [
analyze_indty_tac ~what indtyinfo;
- (fun s -> select_tac
- ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
- distribute_tac (cases ~what) ])
+ (fun s ->
+ select_tac
+ ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true
+ s);
+ (fun s ->
+ distribute_tac
+ (cases ~what:("",0,Ast.NCic (HExtlib.unopt !indtyinfo).term)) s); ])
(match !sort with NCic.Sort x -> x | _ -> assert false))
in
let eliminator =
(match !sort with NCic.Sort x -> x | _ -> assert false))
in
let eliminator =
- let _,_,w = what in
- Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+ let what = (HExtlib.unopt !indtyinfo).term in
+ Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ]
in
exact_tac ("",0,eliminator) status) ])
;;
in
exact_tac ("",0,eliminator) status) ])
;;