diff options
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 43 |
1 files changed, 22 insertions, 21 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index f0c7a3961..0755f8bcf 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -25,6 +25,7 @@ open Tactics open Ind_tables open Misctypes open Proofview.Notations +open Context.Rel.Declaration let out_punivs = Univ.out_punivs @@ -146,17 +147,17 @@ let build_beq_scheme mode kn = ) ext_rel_list in let eq_input = List.fold_left2 - ( fun a b (n,_,_) -> (* mkLambda(n,b,a) ) *) + ( fun a b decl -> (* mkLambda(n,b,a) ) *) (* here I leave the Naming thingy so that the type of the function is more readable for the user *) - mkNamedLambda (eqName n) b a ) + mkNamedLambda (eqName (get_name decl)) b a ) c (List.rev eqs_typ) lnamesparrec in - List.fold_left (fun a (n,_,t) ->(* mkLambda(n,t,a)) eq_input rel_list *) + List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *) (* Same here , hoping the auto renaming will do something good ;) *) mkNamedLambda - (match n with Name s -> s | Anonymous -> Id.of_string "A") - t a) eq_input lnamesparrec + (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (get_type decl) a) eq_input lnamesparrec in let make_one_eq cur = let u = Univ.Instance.empty in @@ -248,7 +249,7 @@ let build_beq_scheme mode kn = | 0 -> Lazy.force tt | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in for ndx = 0 to nb_cstr_args-1 do - let _,_,cc = List.nth constrsi.(i).cs_args ndx in + let cc = get_type (List.nth constrsi.(i).cs_args ndx) in let eqA, eff' = compute_A_equality rel_list nparrec (nparrec+3+2*nb_cstr_args) @@ -267,14 +268,14 @@ let build_beq_scheme mode kn = (Array.sub eqs 1 (nb_cstr_args - 1)) ) in - (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) cc + (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) cc (constrsj.(j).cs_args) ) - else ar2.(j) <- (List.fold_left (fun a (p,q,r) -> - mkLambda (p,r,a)) (Lazy.force ff) (constrsj.(j).cs_args) ) + else ar2.(j) <- (List.fold_left (fun a decl -> + mkLambda (get_name decl, get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) ) done; - ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) + ar.(i) <- (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) (mkCase (ci,do_predicate rel_list nb_cstr_args, mkVar (Id.of_string "Y") ,ar2)) (constrsi.(i).cs_args)) @@ -487,8 +488,8 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = create, from a list of ids [i1,i2,...,in] the list [(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al )] *) -let list_id l = List.fold_left ( fun a (n,_,t) -> let s' = - match n with +let list_id l = List.fold_left ( fun a decl -> let s' = + match get_name decl with Name s -> Id.to_string s | Anonymous -> "A" in (Id.of_string s',Id.of_string ("eq_"^s'), @@ -535,9 +536,9 @@ let compute_bl_goal ind lnamesparrec nparrec = let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> mkNamedProd seq b a ) bl_input (List.rev list_id) (List.rev eqs_typ) in - List.fold_left (fun a (n,_,t) -> mkNamedProd - (match n with Name s -> s | Anonymous -> Id.of_string "A") - t a) eq_input lnamesparrec + List.fold_left (fun a decl -> mkNamedProd + (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in @@ -678,9 +679,9 @@ let compute_lb_goal ind lnamesparrec nparrec = let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> mkNamedProd seq b a ) lb_input (List.rev list_id) (List.rev eqs_typ) in - List.fold_left (fun a (n,_,t) -> mkNamedProd - (match n with Name s -> s | Anonymous -> Id.of_string "A") - t a) eq_input lnamesparrec + List.fold_left (fun a decl -> mkNamedProd + (match (get_name decl) with Name s -> s | Anonymous -> Id.of_string "A") + (get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in @@ -819,9 +820,9 @@ let compute_dec_goal ind lnamesparrec nparrec = let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> mkNamedProd seq b a ) bl_input (List.rev list_id) (List.rev eqs_typ) in - List.fold_left (fun a (n,_,t) -> mkNamedProd - (match n with Name s -> s | Anonymous -> Id.of_string "A") - t a) eq_input lnamesparrec + List.fold_left (fun a decl -> mkNamedProd + (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in |