diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elim.ml | 6 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/inv.ml | 6 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 20 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 14 |
5 files changed, 25 insertions, 23 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index bcb1c05cc..fe36085b8 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -55,7 +55,7 @@ Another example : *) let elimHypThen tac id = - elimination_then tac (mkVar id) + elimination_then tac (EConstr.mkVar id) let rec general_decompose_on_hyp recognizer = ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) @@ -125,7 +125,7 @@ let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) let simple_elimination c = - elimination_then (fun _ -> tclIDTAC) c + elimination_then (fun _ -> tclIDTAC) (EConstr.of_constr c) let induction_trailer abs_i abs_j bargs = tclTHEN @@ -166,7 +166,7 @@ let double_ind h1 h2 = (onLastHypId (fun id -> elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) + (introElimAssumsThen (induction_trailer abs_i abs_j)) (EConstr.mkVar id)))) end } let h_double_induction = double_ind diff --git a/tactics/equality.ml b/tactics/equality.ml index fbf461f6f..fa4164bb9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -985,7 +985,7 @@ let apply_on_clause (f,t) clause = let t = EConstr.of_constr t in let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in let argmv = - (match kind_of_term (last_arg f_clause.evd f_clause.templval.Evd.rebus) with + (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with | Meta mv -> mv | _ -> user_err (str "Ill-formed clause applicator.")) in clenv_fchain ~with_univs:false argmv f_clause clause diff --git a/tactics/inv.ml b/tactics/inv.ml index 2f5186f81..60f1c3542 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -443,7 +443,8 @@ let raw_inversion inv_kind id status names = let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in CErrors.user_err msg in - let IndType (indf,realargs) = find_rectype env sigma (EConstr.of_constr t) in + let t = EConstr.of_constr t in + let IndType (indf,realargs) = find_rectype env sigma t in let evdref = ref sigma in let (elim_predicate, args) = make_inv_predicate env evdref indf realargs id status concl in @@ -463,13 +464,14 @@ let raw_inversion inv_kind id status names = in let neqns = List.length realargs in let as_mode = names != None in + let elim_predicate = EConstr.of_constr elim_predicate in let tac = (tclTHENS (assert_before Anonymous cut_concl) [case_tac names (introCaseAssumsThen false (* ApplyOn not supported by inversion *) (rewrite_equations_tac as_mode inv_kind id neqns)) - (Some elim_predicate) ind (c, t); + (Some elim_predicate) ind (EConstr.of_constr c,t); onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) in Sigma.Unsafe.of_pair (tac, sigma) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 459947051..0546132c1 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -147,9 +147,9 @@ let ifOnHyp pred tac1 tac2 id gl = type branch_args = { ity : pinductive; (* the type we were eliminating on *) - largs : constr list; (* its arguments *) + largs : EConstr.constr list; (* its arguments *) branchnum : int; (* the branch number *) - pred : constr; (* the predicate we used *) + pred : EConstr.constr; (* the predicate we used *) nassums : int; (* number of assumptions/letin to be introduced *) branchsign : bool list; (* the signature of the branch. true=assumption, false=let-in *) @@ -622,8 +622,7 @@ module New = struct (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim isrec allnames tac predicate ind (c, t) = - let c = EConstr.of_constr c in - let t = EConstr.of_constr t in + let open EConstr in Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) @@ -632,13 +631,13 @@ module New = struct (* applying elimination_scheme just a little modified *) let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (EConstr.of_constr elim,EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim)))) gl in let indmv = - match kind_of_term (last_arg elimclause.evd elimclause.templval.Evd.rebus) with + match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with | Meta mv -> mv | _ -> anomaly (str"elimination") in let pmv = - let p, _ = decompose_app (EConstr.Unsafe.to_constr elimclause.templtyp.Evd.rebus) in - match kind_of_term p with + let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in + match EConstr.kind elimclause.evd p with | Meta p -> p | _ -> let name_elim = @@ -657,11 +656,11 @@ module New = struct let elimclause' = match predicate with | None -> elimclause' - | Some p -> clenv_unify ~flags Reduction.CONV (EConstr.mkMeta pmv) (EConstr.of_constr p) elimclause' + | Some p -> clenv_unify ~flags Reduction.CONV (EConstr.mkMeta pmv) p elimclause' in let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in let after_tac i = - let (hd,largs) = decompose_app (EConstr.Unsafe.to_constr clenv'.templtyp.Evd.rebus) in + let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in let ba = { branchsign = branchsigns.(i); branchnames = brnames.(i); nassums = List.length branchsigns.(i); @@ -680,7 +679,8 @@ module New = struct let elimination_then tac c = Proofview.Goal.nf_enter { enter = begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (EConstr.of_constr (pf_unsafe_type_of gl (EConstr.of_constr c))) in + let (ind,t) = pf_reduce_to_quantified_ind gl (EConstr.of_constr (pf_unsafe_type_of gl c)) in + let t = EConstr.of_constr t in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | None -> true,gl_make_elim diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 18cf03c51..974bf83a3 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -97,17 +97,17 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic (** {6 Elimination tacticals. } *) -type branch_args = { +type branch_args = private { ity : pinductive; (** the type we were eliminating on *) - largs : constr list; (** its arguments *) + largs : EConstr.constr list; (** its arguments *) branchnum : int; (** the branch number *) - pred : constr; (** the predicate we used *) + pred : EConstr.constr; (** the predicate we used *) nassums : int; (** number of assumptions/letin to be introduced *) branchsign : bool list; (** the signature of the branch. true=assumption, false=let-in *) branchnames : intro_patterns} -type branch_assumptions = { +type branch_assumptions = private { ba : branch_args; (** the branch args *) assums : Context.Named.t} (** the list of assumptions introduced *) @@ -253,15 +253,15 @@ module New : sig val elimination_then : (branch_args -> unit Proofview.tactic) -> - constr -> unit Proofview.tactic + EConstr.constr -> unit Proofview.tactic val case_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic + EConstr.constr option -> pinductive -> EConstr.constr * EConstr.types -> unit Proofview.tactic val case_nodep_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic + EConstr.constr option -> pinductive -> EConstr.constr * EConstr.types -> unit Proofview.tactic val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic |