diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml | 9 | ||||
| -rw-r--r-- | tactics/elim.ml | 10 | ||||
| -rw-r--r-- | tactics/equality.ml | 91 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 3 | ||||
| -rw-r--r-- | tactics/inv.ml | 37 | ||||
| -rw-r--r-- | tactics/leminv.ml | 15 | ||||
| -rw-r--r-- | tactics/refine.ml | 15 | ||||
| -rw-r--r-- | tactics/tactics.ml | 19 | ||||
| -rw-r--r-- | tactics/tauto.ml | 4 |
10 files changed, 104 insertions, 101 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index acf0b6cc6..953f2f74a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -728,7 +728,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal = (tclTRY_sign decomp_empty_term extra_sign) :: (List.map - (fun id -> tclTHEN (decomp_unary_term (VAR id)) + (fun id -> tclTHEN (decomp_unary_term (mkVar id)) (tclTHEN (clear_one id) (search_gen decomp p db_list local_db []))) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index bad9866f6..93e8e6c3a 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -18,7 +18,7 @@ open Auto let e_give_exact c gl = tclTHEN (unify (pf_type_of gl c)) (Tactics.exact c) gl -let assumption id = e_give_exact (VAR id) +let assumption id = e_give_exact (mkVar id) let e_assumption gl = tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl @@ -26,7 +26,7 @@ let e_assumption gl = let e_give_exact_constr = hide_constr_tactic "EExact" e_give_exact let registered_e_assumption gl = - tclFIRST (List.map (fun id gl -> e_give_exact_constr (VAR id) gl) + tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) (pf_ids_of_hyps gl)) gl let e_resolve_with_bindings_tac (c,lbind) gl = @@ -53,8 +53,7 @@ let vernac_e_resolve_constr = let one_step l gl = [Tactics.intro] - @ (List.map e_resolve_constr (List.map (fun x -> VAR x) - (pf_ids_of_hyps gl))) + @ (List.map e_resolve_constr (List.map mkVar (pf_ids_of_hyps gl))) @ (List.map e_resolve_constr l) @ (List.map assumption (pf_ids_of_hyps gl)) @@ -197,7 +196,7 @@ let e_possible_resolve db_list local_db gl = (* A version with correct (?) backtracking using operations on lists of goals *) -let assumption_tac_list id = apply_tac_list (e_give_exact_constr (VAR id)) +let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id)) exception Nogoals diff --git a/tactics/elim.ml b/tactics/elim.ml index 2cfcd8559..fc0dec451 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -54,7 +54,7 @@ Another example : *) let elimClauseThen tac idopt gl = - elimination_then tac ([],[]) (VAR (out_some idopt)) gl + elimination_then tac ([],[]) (mkVar (out_some idopt)) gl let rec general_decompose_clause recognizer = ifOnClause recognizer @@ -145,14 +145,14 @@ let induction_trailer abs_i abs_j bargs = (onLastHyp (fun idopt gls -> let id = out_some idopt in - let idty = pf_type_of gls (VAR id) in + let idty = pf_type_of gls (mkVar id) in let fvty = global_vars idty in let possible_bring_ids = (List.tl (List.map out_some (nLastHyps (abs_j - abs_i) gls))) @bargs.assums in let (ids,_) = List.fold_left (fun (bring_ids,leave_ids) cid -> - let cidty = pf_type_of gls (VAR cid) in + let cidty = pf_type_of gls (mkVar cid) in if not (List.mem cid leave_ids) then (cid::bring_ids,leave_ids) else (bring_ids,cid::leave_ids)) @@ -160,7 +160,7 @@ let induction_trailer abs_i abs_j bargs = in (tclTHEN (tclTHEN (bring_hyps (List.map in_some ids)) (clear_clauses (List.rev (List.map in_some ids)))) - (simple_elimination (VAR id))) gls)) + (simple_elimination (mkVar id))) gls)) let double_ind abs_i abs_j gls = let cl = pf_concl gls in @@ -169,7 +169,7 @@ let double_ind abs_i abs_j gls = (fun idopt -> elimination_then (introElimAssumsThen (induction_trailer abs_i abs_j)) - ([],[]) (VAR (out_some idopt))))) gls + ([],[]) (mkVar (out_some idopt))))) gls let dyn_double_ind = function | [Integer i; Integer j] -> double_ind i j diff --git a/tactics/equality.ml b/tactics/equality.ml index 2b9b23011..03e4688aa 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -94,10 +94,10 @@ let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl = and t2 = pf_type_of gl c2 in if unsafe or (pf_conv_x gl t1 t2) then let (e,sym) = - match hnf_type_of gl t1 with - | DOP0(Sort(Prop(Pos))) -> (eq,sym_eq) - | DOP0(Sort(Type(_))) -> (eqt,sym_eqt) - | _ -> error "replace" + match kind_of_term (hnf_type_of gl t1) with + | IsSort (Prop(Pos)) -> (eq,sym_eq) + | IsSort (Type(_)) -> (eqt,sym_eqt) + | _ -> error "replace" in (tclTHENL (elim_type (applist (e, [t1;c1;c2]))) (tclORELSE assumption @@ -343,24 +343,25 @@ exception DiscrFound of (sorts oper * int) list * sorts oper * sorts oper let find_positions env sigma t1 t2 = let rec findrec posn t1 t2 = - match (whd_betadeltaiota_stack env sigma t1, - whd_betadeltaiota_stack env sigma t2) with + let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in + let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in + match (kind_of_term hd1, kind_of_term hd2) with - | ((DOPN(MutConstruct sp1 as oper1,_) as hd1,args1), - (DOPN(MutConstruct sp2 as oper2,_) as hd2,args2)) -> + | IsMutConstruct (sp1,_), IsMutConstruct (sp2,_) -> (* both sides are constructors, so either we descend, or we can discriminate here. *) if sp1 = sp2 then List.flatten (list_map2_i - (fun i arg1 arg2 -> findrec ((oper1,i)::posn) arg1 arg2) + (fun i arg1 arg2 -> + findrec ((MutConstruct sp1,i)::posn) arg1 arg2) 0 args1 args2) else - raise (DiscrFound(List.rev posn,oper1,oper2)) + raise (DiscrFound(List.rev posn,MutConstruct sp1,MutConstruct sp2)) - | (t1_0,t2_0) -> - let t1_0 = applist t1_0 - and t2_0 = applist t2_0 in + | _ -> + let t1_0 = applist (hd1,args1) + and t2_0 = applist (hd2,args2) in if is_conv env sigma t1_0 t2_0 then [] else @@ -524,7 +525,7 @@ let rec build_discriminator sigma env dirn c sort = function let _,arsort = get_arity indf in let nparams = mis_nparams (fst (dest_ind_family indf)) in let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in - let newc = Rel(cnum_nlams-(argnum-nparams)) in + let newc = mkRel(cnum_nlams-(argnum-nparams)) in let subval = build_discriminator sigma cnum_env dirn newc sort l in (match necessary_elimination arsort (destSort sort) with | Type_Type -> @@ -546,7 +547,7 @@ let gen_absurdity id gl = if (pf_is_matching gl (pat_False ()) (clause_type (Some id) gl)) or (pf_is_matching gl (pat_EmptyT ()) (clause_type (Some id) gl)) then - simplest_elim (VAR id) gl + simplest_elim (mkVar id) gl else errorlabstrm "Equality.gen_absurdity" [< 'sTR "Not the negation of an equality" >] @@ -575,7 +576,7 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls = let absurd_term = build_EmptyT () in let h = pf_get_new_id (id_of_string "HH")gls in let pred= mkNamedLambda e t - (mkNamedLambda h (applist (eq_term, [t;t1;(Rel 1)])) + (mkNamedLambda h (applist (eq_term, [t;t1;(mkRel 1)])) discriminator) in (applist(eq_elim, [t;t1;pred;i;t2]), absurd_term) @@ -608,7 +609,7 @@ let discr id gls = push_var_decl (e,assumption_of_judgment env sigma tj) env in let discriminator = - build_discriminator sigma e_env dirn (VAR e) sort cpath in + build_discriminator sigma e_env dirn (mkVar e) sort cpath in let (indt,_) = find_mrectype env sigma t in let arity = Global.mind_arity indt in let (pf, absurd_term) = @@ -616,7 +617,7 @@ let discr id gls = in tclCOMPLETE((tclTHENS (cut_intro absurd_term) ([onLastHyp (compose gen_absurdity out_some); - refine (mkAppL (pf, [| VAR id |]))]))) gls + refine (mkAppL (pf, [| mkVar id |]))]))) gls | _ -> assert false) let not_found_message id = @@ -696,9 +697,9 @@ let find_sigma_data s = If [rty] depends on lind, then we will build the term - (existS A==[type_of(Rel lind)] P==(Lambda(na:type_of(Rel lind), + (existS A==[type_of(mkRel lind)] P==(Lambda(na:type_of(mkRel lind), [rty{1/lind}])) - [(Rel lind)] [rterm]) + [(mkRel lind)] [rterm]) which should have type (sigS A P) - we can verify it by typechecking at the end. @@ -708,12 +709,12 @@ let make_tuple env sigma (rterm,rty) lind = if dependent (mkRel lind) rty then let {intro = exist_term; ex = sig_term} = find_sigma_data (get_sort_of env sigma rty) in - let a = type_of env sigma (Rel lind) in - (* We replace (Rel lind) by (Rel 1) in rty then abstract on (na:a) *) - let rty' = substnl [Rel 1] lind rty in + let a = type_of env sigma (mkRel lind) in + (* We replace (mkRel lind) by (mkRel 1) in rty then abstract on (na:a) *) + let rty' = substnl [mkRel 1] lind rty in let na = fst (lookup_rel_type lind env) in let p = mkLambda (na, a, rty') in - (applist(exist_term,[a;p;(Rel lind);rterm]), + (applist(exist_term,[a;p;(mkRel lind);rterm]), applist(sig_term,[a;p])) else (rterm,rty) @@ -839,7 +840,7 @@ let rec build_injrec sigma env (t1,t2) c = function let (ity,_) = find_mrectype env sigma cty in let nparams = Global.mind_nparams ity in let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in - let newc = Rel(cnum_nlams-(argnum-nparams)) in + let newc = mkRel(cnum_nlams-(argnum-nparams)) in let (subval,tuplety,dfltval) = build_injrec sigma cnum_env (t1,t2) newc l in @@ -891,7 +892,7 @@ let inj id gls = map_succeed (fun (cpath,t1_0,t2_0) -> let (injbody,resty) = - build_injector sigma e_env (t1_0,t2_0) (VAR e) cpath in + build_injector sigma e_env (t1_0,t2_0) (mkVar e) cpath in let injfun = mkNamedLambda e t injbody in try let _ = type_of env sigma injfun in (injfun,resty) @@ -907,7 +908,7 @@ let inj id gls = [t;resty;injfun; try_delta_expand env sigma t1; try_delta_expand env sigma t2; - VAR id]) + mkVar id]) in let ty = pf_type_of gls pf in ((tclTHENS (cut ty) ([tclIDTAC;refine pf])))) @@ -953,13 +954,13 @@ let decompEqThen ntac id gls = let e_env = push_var_decl (e,assumption_of_judgment env sigma tj) env in let discriminator = - build_discriminator sigma e_env dirn (VAR e) sort cpath in + build_discriminator sigma e_env dirn (mkVar e) sort cpath in let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq gls in tclCOMPLETE ((tclTHENS (cut_intro absurd_term) ([onLastHyp (compose gen_absurdity out_some); - refine (mkAppL (pf, [| VAR id |]))]))) gls + refine (mkAppL (pf, [| mkVar id |]))]))) gls | Inr posns -> (let e = pf_get_new_id (id_of_string "e") gls in let e_env = @@ -968,7 +969,7 @@ let decompEqThen ntac id gls = map_succeed (fun (cpath,t1_0,t2_0) -> let (injbody,resty) = - build_injector sigma e_env (t1_0,t2_0) (VAR e) cpath in + build_injector sigma e_env (t1_0,t2_0) (mkVar e) cpath in let injfun = mkNamedLambda e t injbody in try let _ = type_of env sigma injfun in (injfun,resty) @@ -982,7 +983,7 @@ let decompEqThen ntac id gls = (tclMAP (fun (injfun,resty) -> let pf = applist(get_squel lbeq.congr, [t;resty;injfun;t1;t2; - VAR id]) in + mkVar id]) in let ty = pf_type_of gls pf in ((tclTHENS (cut ty) ([tclIDTAC;refine pf])))) @@ -1047,7 +1048,7 @@ let swapEquandsInConcl gls = let swapEquandsInHyp id gls = ((tclTHENS (cut_replacing id (swap_equands gls (clause_type (Some id) gls))) ([tclIDTAC; - (tclTHEN (swapEquandsInConcl) (exact (VAR id)))]))) gls + (tclTHEN (swapEquandsInConcl) (exact (mkVar id)))]))) gls (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. It yields the boolean true wether @@ -1070,19 +1071,19 @@ let find_elim sort_of_gl lbeq = (* builds a predicate [e:t][H:(lbeq t e t1)](body e) to be used as an argument for equality dependent elimination principle: - Preconditon: dependent body (Rel 1) *) + Preconditon: dependent body (mkRel 1) *) let build_dependent_rewrite_predicate (t,t1,t2) body lbeq gls = let e = pf_get_new_id (id_of_string "e") gls in let h = pf_get_new_id (id_of_string "HH") gls in let eq_term = get_squel lbeq.eq in (mkNamedLambda e t - (mkNamedLambda h (applist (eq_term, [t;t1;(Rel 1)])) + (mkNamedLambda h (applist (eq_term, [t;t1;(mkRel 1)])) (lift 1 body))) (* builds a predicate [e:t](body e) ??? to be used as an argument for equality non-dependent elimination principle: - Preconditon: dependent body (Rel 1) *) + Preconditon: dependent body (mkRel 1) *) let build_non_dependent_rewrite_predicate (t,t1,t2) body gls = lambda_create (pf_env gls) (t,body) @@ -1113,13 +1114,13 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls = and B might contain instances of the ei, we will return the term: ([x1:ty(e1)]...[xn:ty(en)]B - (projS1 (Rel 1)) - (projS1 (projS2 (Rel 1))) + (projS1 (mkRel 1)) + (projS1 (projS2 (mkRel 1))) ... etc ...) That is, we will abstract out the terms e1...en+1 as usual, but will then produce a term in which the abstraction is on a single - term - the debruijn index [Rel 1], which will be of the same type + term - the debruijn index [mkRel 1], which will be of the same type as dep_pair. ALGORITHM for abstraction: @@ -1168,7 +1169,7 @@ let decomp_tuple_term env c t = with e when catchable_exception e -> [((ex,exty),inner_code)] in - List.split (decomprec (Rel 1) c t) + List.split (decomprec (mkRel 1) c t) (* let whd_const_state namelist env sigma = @@ -1198,7 +1199,7 @@ let subst_tuple_term env sigma dep_pair b = List.fold_right (fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in let app_B = applist(abst_B,proj_list) in - (* inutile ?? les projs sont appliquées à (Rel 1) ?? *) + (* inutile ?? les projs sont appliquées à (mkRel 1) ?? *) (* let { proj1 = proj1_sp; proj2 = proj2_sp; elim = sig_elim_sp } = find_sigma_data (get_sort_of env sigma typ) in @@ -1236,7 +1237,7 @@ let substInHyp eqn id gls = (tclTHENS (cut_replacing id (subst1 e2 body)) ([tclIDTAC; (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2)) - ([exact (VAR id);tclIDTAC]))])) gls + ([exact (mkVar id);tclIDTAC]))])) gls let revSubstInHyp eqn id gls = (tclTHENS (substInHyp (swap_equands gls eqn) id) @@ -1500,10 +1501,10 @@ let hypSubst id cls gls = match cls with | None -> (tclTHENS (substInConcl (clause_type (Some id) gls)) - ([tclIDTAC; exact (VAR id)])) gls + ([tclIDTAC; exact (mkVar id)])) gls | Some hypid -> (tclTHENS (substInHyp (clause_type (Some id) gls) hypid) - ([tclIDTAC;exact (VAR id)])) gls + ([tclIDTAC;exact (mkVar id)])) gls (* id:a=b |- (P a) * HypSubst id. @@ -1555,10 +1556,10 @@ let revHypSubst id cls gls = match cls with | None -> (tclTHENS (revSubstInConcl (clause_type (Some id) gls)) - ([tclIDTAC; exact (VAR id)])) gls + ([tclIDTAC; exact (mkVar id)])) gls | Some hypid -> (tclTHENS (revSubstInHyp (clause_type (Some id) gls) hypid) - ([tclIDTAC;exact (VAR id)])) gls + ([tclIDTAC;exact (mkVar id)])) gls (* id:a=b |- (P b) * HypSubst id. diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index cc88fbcd7..d9d81238b 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -67,8 +67,7 @@ let get_reference mods s = let soinstance squel arglist = let mvs,c = get_squel_core squel in let mvb = List.combine mvs arglist in - Sosub.soexecute (Reduction.strong (fun _ _ -> Reduction.whd_meta mvb) - empty_env Evd.empty c) + Reduction.local_strong (Reduction.whd_meta mvb) c let get_squel m = let mvs, c = get_squel_core m in diff --git a/tactics/inv.ml b/tactics/inv.ml index 0a09c441b..42dcb18f5 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -77,7 +77,7 @@ type inversion_status = Dep of constr option | NoDep let compute_eqn env sigma n i ai = (ai,get_type_of env sigma ai), - (Rel (n-i),get_type_of env sigma (Rel (n-i))) + (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) let make_inv_predicate env sigma ind id status concl = let indf,realargs = dest_ind_type ind in @@ -90,7 +90,7 @@ let make_inv_predicate env sigma ind id status concl = let env' = push_rels hyps_arity env in (hyps_arity,concl) | Dep dflt_concl -> - if not (dependent (VAR id) concl) then + if not (dependent (mkVar id) concl) then errorlabstrm "make_inv_predicate" [< 'sTR "Current goal does not depend on "; print_id id >]; (* We abstract the conclusion of goal with respect to @@ -102,7 +102,7 @@ let make_inv_predicate env sigma ind id status concl = | None -> let sort = get_sort_of env sigma concl in let p = make_arity env true indf sort in - abstract_list_all env sigma p concl (realargs@[VAR id]) + abstract_list_all env sigma p concl (realargs@[mkVar id]) in let hyps,_ = decompose_lam_n (nrealargs+1) pred in let c3 = whd_beta (applist (pred,rel_list nrealargs (nrealargs +1))) @@ -114,9 +114,9 @@ let make_inv_predicate env sigma ind id status concl = let realargs' = List.map (lift nhyps) realargs in let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in (* Now the arity is pushed, and we need to construct the pairs - * ai,Rel(n-i+1) *) - (* Now, we can recurse down this list, for each ai,(Rel k) whether to - push <Ai>(Rel k)=ai (when Ai is closed). + * ai,mkRel(n-i+1) *) + (* Now, we can recurse down this list, for each ai,(mkRel k) whether to + push <Ai>(mkRel k)=ai (when Ai is closed). In any case, we carry along the rest of pairs *) let rec build_concl eqns n = function | [] -> (prod_it concl eqns,n) @@ -180,10 +180,10 @@ let make_inv_predicate env sigma ind id status concl = let introsReplacing = intros_replacing (* déplacé *) (* Computes the subset of hypothesis in the local context whose - type depends on t (should be of the form (VAR id)), then + type depends on t (should be of the form (mkVar id)), then it generalizes them, applies tac to rewrite all occurrencies of t, and introduces generalized hypotheis. - Precondition: t=(VAR id) *) + Precondition: t=(mkVar id) *) let rec dependent_hyps id idlist sign = let rec dep_rec =function @@ -229,22 +229,23 @@ let projectAndApply thin cls depids gls = let subst_hyp gls = let orient_rule cls = let (t,t1,t2) = dest_eq gls (clause_type cls gls) in - match (strip_outer_cast t1, strip_outer_cast t2) with - | (VAR id1, _) -> generalizeRewriteIntros (subst_hyp_LR cls) depids id1 - | (_, VAR id2) -> generalizeRewriteIntros (subst_hyp_RL cls) depids id2 + match (kind_of_term (strip_outer_cast t1), + kind_of_term (strip_outer_cast t2)) with + | IsVar id1, _ -> generalizeRewriteIntros (subst_hyp_LR cls) depids id1 + | _, IsVar id2 -> generalizeRewriteIntros (subst_hyp_RL cls) depids id2 | _ -> subst_hyp_RL cls in onLastHyp orient_rule gls in let (t,t1,t2) = dest_eq gls (clause_type cls gls) in - match (thin, strip_outer_cast t1, strip_outer_cast t2) with - | (true, VAR id1, _) -> generalizeRewriteIntros + match (thin, kind_of_term (strip_outer_cast t1), kind_of_term (strip_outer_cast t2)) with + | (true, IsVar id1, _) -> generalizeRewriteIntros (tclTHEN (subst_hyp_LR cls) (clear_clause cls)) depids id1 gls - | (false, VAR id1, _) -> + | (false, IsVar id1, _) -> generalizeRewriteIntros (subst_hyp_LR cls) depids id1 gls - | (true, _ , VAR id2) -> generalizeRewriteIntros + | (true, _ , IsVar id2) -> generalizeRewriteIntros (tclTHEN (subst_hyp_RL cls) (clear_clause cls)) depids id2 gls - | (false, _ , VAR id2) -> + | (false, _ , IsVar id2) -> generalizeRewriteIntros (subst_hyp_RL cls) depids id2 gls | (true, _, _) -> let deq_trailer neqns = @@ -321,7 +322,7 @@ let case_trailer othin neqns ba gl = let res_case_then gene thin indbinding id status gl = let env = pf_env gl and sigma = project gl in - let c = VAR id in + let c = mkVar id in let (wc,kONT) = startWalk gl in let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in let indclause = mk_clenv_from wc (c,t) in @@ -348,7 +349,7 @@ let res_case_then gene thin indbinding id status gl = [onLastHyp (fun cls-> (tclTHEN (applyUsing - (applist(VAR (out_some cls), + (applist(mkVar (out_some cls), list_tabulate (fun _ -> mkMeta(new_meta())) neqns))) Auto.default_auto)); diff --git a/tactics/leminv.ml b/tactics/leminv.ml index c5bf51771..1e115c671 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -127,12 +127,12 @@ let rec add_prods_sign env sigma t = match kind_of_term (whd_betadeltaiota env sigma t) with | IsProd (na,c1,b) -> let id = Environ.id_of_name_using_hdchar env t na in - let b'= subst1 (VAR id) b in + let b'= subst1 (mkVar id) b in let j = Retyping.get_assumption_of env sigma c1 in add_prods_sign (Environ.push_var_decl (id,j) env) sigma b' | IsLetIn (na,c1,t1,b) -> let id = Environ.id_of_name_using_hdchar env t na in - let b'= subst1 (VAR id) b in + let b'= subst1 (mkVar id) b in let j = Retyping.get_assumption_of env sigma t1 in add_prods_sign (Environ.push_var_def (id,c1,j) env) sigma b' | _ -> (env,t) @@ -158,7 +158,8 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = if dep_option then let pty = make_arity env true indf sort in let goal = - mkProd (Anonymous, mkAppliedInd ind, applist(VAR p,realargs@[Rel 1])) + mkProd + (Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1])) in pty,goal else @@ -167,11 +168,11 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let revargs,ownsign = fold_var_context (fun env (id,_,_ as d) (revargs,hyps) -> - if List.mem id ivars then ((VAR id)::revargs,add_var d hyps) + if List.mem id ivars then ((mkVar id)::revargs,add_var d hyps) else (revargs,hyps)) env ([],[]) in let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in - let goal = mkArrow i (applist(VAR p, List.rev revargs)) in + let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in (pty,goal) in let npty = nf_betadeltaiota env sigma pty in @@ -215,7 +216,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = List.fold_left (fun (avoid,sign,mvb) (mv,mvty) -> let h = next_ident_away (id_of_string "H") avoid in - (h::avoid, add_var_decl (h,mvty) sign, (mv,VAR h)::mvb)) + (h::avoid, add_var_decl (h,mvty) sign, (mv,mkVar h)::mvb)) (ids_of_context invEnv, ownSign, []) meta_types in let invProof = @@ -322,7 +323,7 @@ let lemInv id c gls = try let (wc,kONT) = startWalk gls in let clause = mk_clenv_type_of wc c in - let clause = clenv_constrain_with_bindings [(Abs (-1),VAR id)] clause in + let clause = clenv_constrain_with_bindings [(Abs (-1),mkVar id)] clause in res_pf kONT clause gls with (* Ce n'est pas l'endroit pour cela diff --git a/tactics/refine.ml b/tactics/refine.ml index ce60df06a..75f22c4ff 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -134,13 +134,13 @@ let rec compute_metamap env c = match kind_of_term c with | IsCast (m,ty) when isMeta m -> TH (c,[destMeta m,ty],[None]) (* abstraction => il faut décomposer si le terme dessous n'est pas pur - * attention : dans ce cas il faut remplacer (Rel 1) par (VAR x) + * attention : dans ce cas il faut remplacer (Rel 1) par (Var x) * où x est une variable FRAICHE *) | IsLambda (name,c1,c2) -> let v = fresh env name in let tj = Retyping.get_assumption_of env Evd.empty c1 in let env' = push_var_decl (v,tj) env in - begin match compute_metamap env' (subst1 (VAR v) c2) with + begin match compute_metamap env' (subst1 (mkVar v) c2) with (* terme de preuve complet *) | TH (_,_,[]) -> TH (c,[],[]) (* terme de preuve incomplet *) @@ -162,14 +162,15 @@ let rec compute_metamap env c = match kind_of_term c with TH (c,[],[]) end - | IsMutCase _ -> + | IsMutCase (ci,p,c,v) -> (* bof... *) - let op,v = - match c with DOPN(MutCase _ as op,v) -> (op,v) | _ -> assert false in + let v = Array.append [|p;c|] v in let a = Array.map (compute_metamap env) v in begin try - let v',mm,sgp = replace_in_array env a in TH (DOPN(op,v'),mm,sgp) + let v',mm,sgp = replace_in_array env a in + let v'' = Array.sub v' 2 (Array.length v) in + TH (mkMutCase (ci,v'.(0),v'.(1),v''),mm,sgp) with NoMeta -> TH (c,[],[]) end @@ -185,7 +186,7 @@ let rec compute_metamap env c = match kind_of_term c with in let a = Array.map (compute_metamap env') - (Array.map (substl (List.map (fun x -> VAR x) vi)) v) + (Array.map (substl (List.map mkVar vi)) v) in begin try diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 60ea7e8d0..6c4665fd3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -213,7 +213,7 @@ let dyn_change = function (* A function which reduces accordingly to a reduction expression, as the command Eval does. *) -let reduce redexp cl goal = +let reduce redexp cl goal = redin_combinator (reduction_of_redexp redexp) cl goal let dyn_reduce = function @@ -265,6 +265,7 @@ let default_id gl = | IsSort (Prop _) -> (id_of_name_with_default "H" name) | IsSort (Type _) -> (id_of_name_with_default "X" name) | _ -> anomaly "Wrong sort") + | IsLetIn (name,b,_,_) -> id_of_name_using_hdchar (pf_env gl) b name | _ -> error "Introduction needs a product" (* Non primitive introduction tactics are treated by central_intro @@ -293,12 +294,12 @@ let rec central_intro name_flag move_flag force_flag gl = | None -> introduction id gl | Some dest -> tclTHEN (introduction id) (move_hyp true id dest) gl end - with (UserError ("Introduction needs a product",_)) as e -> + with RefinerError IntroNeedsProduct as e -> if force_flag then try - ((tclTHEN (reduce Red []) (central_intro name_flag move_flag - force_flag)) gl) - with UserError ("Term not reducible",_) -> + ((tclTHEN (reduce (Red true) []) + (central_intro name_flag move_flag force_flag)) gl) + with Redelimination -> errorlabstrm "Intro" [<'sTR "No product even after head-reduction">] else @@ -349,8 +350,8 @@ let rec intros_until s g = | Some depth -> tclDO depth intro g | None -> try - ((tclTHEN (reduce Red []) (intros_until s)) g) - with UserError ("Term not reducible",_) -> + ((tclTHEN (reduce (Red true) []) (intros_until s)) g) + with Redelimination -> errorlabstrm "Intros" [<'sTR "No such hypothesis in current goal"; 'sTR " even after head-reduction" >] @@ -360,8 +361,8 @@ let rec intros_until_n n g = | Some depth -> tclDO depth intro g | None -> try - ((tclTHEN (reduce Red []) (intros_until_n n)) g) - with UserError ("Term not reducible",_) -> + ((tclTHEN (reduce (Red true) []) (intros_until_n n)) g) + with Redelimination -> errorlabstrm "Intros" [<'sTR "No such hypothesis in current goal"; 'sTR " even after head-reduction" >] diff --git a/tactics/tauto.ml b/tactics/tauto.ml index 171eea17b..737ce8a33 100644 --- a/tactics/tauto.ml +++ b/tactics/tauto.ml @@ -1762,7 +1762,7 @@ let rec cci_of_tauto_fml () = let search env id = try - Rel (fst (lookup_rel_id id (Environ.rel_context env))) + mkRel (fst (lookup_rel_id id (Environ.rel_context env))) with Not_found -> if mem_var_context id (Environ.var_context env) then mkVar id @@ -1783,7 +1783,7 @@ let cci_of_tauto_term env t = and ci = global_reference CCI (id_of_string "I") in let rec ter_constr l = function - | TVar x -> (try (try Rel(pos_lis x l) + | TVar x -> (try (try mkRel(pos_lis x l) with TacticFailure -> search env (id_of_string x)) with _ -> raise TacticFailure) |