aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml20
-rw-r--r--tactics/contradiction.ml9
-rw-r--r--tactics/eauto.ml4
-rw-r--r--tactics/elim.ml5
-rw-r--r--tactics/eqschemes.ml10
-rw-r--r--tactics/equality.ml24
-rw-r--r--tactics/hints.ml7
-rw-r--r--tactics/hipattern.ml6
-rw-r--r--tactics/inv.ml13
-rw-r--r--tactics/leminv.ml6
-rw-r--r--tactics/taccoerce.ml344
-rw-r--r--tactics/taccoerce.mli96
-rw-r--r--tactics/tactic_matching.ml8
-rw-r--r--tactics/tacticals.ml13
-rw-r--r--tactics/tactics.ml118
-rw-r--r--tactics/tactics.mllib1
16 files changed, 129 insertions, 555 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6e01a676a2..f9f8e8715e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -32,6 +32,8 @@ open Misctypes
open Proofview.Notations
open Hints
+module NamedDecl = Context.Named.Declaration
+
(** Hint database named "typeclass_instances", now created directly in Auto *)
(** Options handling *)
@@ -523,9 +525,8 @@ let evars_to_goals p evm =
(** Making local hints *)
let make_resolve_hyp env sigma st flags only_classes pri decl =
- let open Context.Named.Declaration in
- let id = get_id decl in
- let cty = Evarutil.nf_evar sigma (get_type decl) in
+ let id = NamedDecl.get_id decl in
+ let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in
let rec iscl env ty =
let ctx, ar = decompose_prod_assum ty in
match kind_of_term (fst (decompose_app ar)) with
@@ -564,10 +565,9 @@ let make_hints g st only_classes sign =
List.fold_left
(fun hints hyp ->
let consider =
- let open Context.Named.Declaration in
- try let t = Global.lookup_named (get_id hyp) |> get_type in
+ try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in
(* Section variable, reindex only if the type changed *)
- not (Term.eq_constr t (get_type hyp))
+ not (Term.eq_constr t (NamedDecl.get_type hyp))
with Not_found -> true
in
if consider then
@@ -1500,9 +1500,11 @@ let head_of_constr h c =
let c = head_of_constr c in
letin_tac None (Name h) c None Locusops.allHyps
-let not_evar c = match kind_of_term c with
-| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
-| _ -> Proofview.tclUNIT ()
+let not_evar c =
+ Proofview.tclEVARMAP >>= fun sigma ->
+ match Evarutil.kind_of_term_upto sigma c with
+ | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
+ | _ -> Proofview.tclUNIT ()
let is_ground c gl =
if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c3796b4842..c81705c1a0 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -13,7 +13,8 @@ open Coqlib
open Reductionops
open Misctypes
open Proofview.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
(* Absurd *)
@@ -46,7 +47,7 @@ let absurd c = absurd c
let filter_hyp f tac =
let rec seek = function
| [] -> Proofview.tclZERO Not_found
- | d::rest when f (get_type d) -> tac (get_id d)
+ | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d)
| _::rest -> seek rest in
Proofview.Goal.enter { enter = begin fun gl ->
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
@@ -60,8 +61,8 @@ let contradiction_context =
let rec seek_neg l = match l with
| [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
| d :: rest ->
- let id = get_id d in
- let typ = nf_evar sigma (get_type d) in
+ let id = NamedDecl.get_id d in
+ let typ = nf_evar sigma (NamedDecl.get_type d) in
let typ = whd_all env sigma typ in
if is_empty_type typ then
simplest_elim (mkVar id)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 6308ab259c..ba21950707 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -29,9 +29,9 @@ open Proofview.Notations
let eauto_unif_flags = auto_flags_of_state full_transparent_state
let e_give_exact ?(flags=eauto_unif_flags) c =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let t1 = Tacmach.New.pf_unsafe_type_of gl c in
- let t2 = Tacmach.New.pf_concl gl in
+ let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
if occur_existential t1 || occur_existential t2 then
Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
else exact_check c
diff --git a/tactics/elim.ml b/tactics/elim.ml
index f2b9eec4b2..3f0c01a29c 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -16,7 +16,8 @@ open Tacmach.New
open Tacticals.New
open Tactics
open Proofview.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
(* Supposed to be called without as clause *)
let introElimAssumsThen tac ba =
@@ -139,7 +140,7 @@ let induction_trailer abs_i abs_j bargs =
let (hyps,_) =
List.fold_left
(fun (bring_ids,leave_ids) d ->
- let cid = get_id d in
+ let cid = NamedDecl.get_id d in
if not (List.mem cid leave_ids)
then (d::bring_ids,leave_ids)
else (bring_ids,cid::leave_ids))
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 1a45217a4a..c94dcfa9df 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -60,6 +60,8 @@ open Indrec
open Sigma.Notations
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+
let hid = Id.of_string "H"
let xid = Id.of_string "X"
let default_id_of_sort = function InProp | InSet -> hid | InType -> xid
@@ -600,9 +602,9 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
| hp :: p :: ind :: indargs ->
let c' =
my_it_mkLambda_or_LetIn indargs
- (mkLambda_or_LetIn (map_constr (liftn (-1) 1) p)
- (mkLambda_or_LetIn (map_constr (liftn (-1) 2) hp)
- (mkLambda_or_LetIn (map_constr (lift 2) ind)
+ (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p)
+ (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
+ (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
(Reductionops.whd_beta Evd.empty
(applist (c,
Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
@@ -741,7 +743,7 @@ let build_congr env (eq,refl,ctx) ind =
if List.exists is_local_def realsign then
error "Inductive equalities with local definitions in arity not supported.";
let env_with_arity = push_rel_context arityctxt env in
- let ty = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
+ let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 24abd1e126..d4b372837d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -45,6 +45,8 @@ open Proofview.Notations
open Unification
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
(* Options *)
let discriminate_introduction = ref true
@@ -629,7 +631,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
in
match evd with
| None ->
- tclFAIL 0 (str"Terms do not have convertible types.")
+ tclFAIL 0 (str"Terms do not have convertible types")
| Some evd ->
let e = build_coq_eq () in
let sym = build_coq_eq_sym () in
@@ -1662,13 +1664,13 @@ exception FoundHyp of (Id.t * constr * bool)
(* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *)
let is_eq_x gl x d =
- let id = get_id d in
+ let id = NamedDecl.get_id d in
try
let is_var id c = match kind_of_term c with
| Var id' -> Id.equal id id'
| _ -> false
in
- let c = pf_nf_evar gl (get_type d) in
+ let c = pf_nf_evar gl (NamedDecl.get_type d) in
let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true));
if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false))
@@ -1686,7 +1688,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
(* The set of hypotheses using x *)
let dephyps =
List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) ->
- let id = get_id dcl in
+ let id = NamedDecl.get_id dcl in
if not (Id.equal id hyp)
&& List.exists (fun y -> occur_var_in_decl env y dcl) deps
then
@@ -1715,9 +1717,9 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
let subst_one_var dep_proof_ok x =
Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
- let xval = pf_get_hyp x gl |> get_value in
+ let decl = pf_get_hyp x gl in
(* If x has a body, simply replace x with body and clear x *)
- if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) else
+ if is_local_def decl then tclTHEN (unfold_body x) (clear [x]) else
(* Find a non-recursive definition for x *)
let res =
try
@@ -1763,12 +1765,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
let find_eq_data_decompose = find_eq_data_decompose gl in
let test decl =
try
- let lbeq,u,(_,x,y) = find_eq_data_decompose (get_type decl) in
+ let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
match kind_of_term x, kind_of_term y with
| Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) ->
- Some (get_id decl)
+ Some (NamedDecl.get_id decl)
| _ ->
None
with Constr_matching.PatternMatchingFailure -> None
@@ -1782,7 +1784,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
let find_eq_data_decompose = find_eq_data_decompose gl in
- let c = pf_get_hyp hyp gl |> get_type in
+ let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
let _,_,(_,x,y) = find_eq_data_decompose c in
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if Term.eq_constr x y then Proofview.tclUNIT () else
@@ -1851,10 +1853,10 @@ let rewrite_assumption_cond cond_eq_term cl =
let rec arec hyps gl = match hyps with
| [] -> error "No such assumption."
| hyp ::rest ->
- let id = get_id hyp in
+ let id = NamedDecl.get_id hyp in
begin
try
- let dir = cond_eq_term (get_type hyp) gl in
+ let dir = cond_eq_term (NamedDecl.get_type hyp) gl in
general_rewrite_clause dir false (mkVar id,NoBindings) cl
with | Failure _ | UserError _ -> arec rest gl
end
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 841f35e9c3..4b43a9e696 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -34,7 +34,8 @@ open Tacred
open Printer
open Vernacexpr
open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
(****************************************)
(* General functions *)
@@ -782,11 +783,11 @@ let make_resolves env sigma flags pri poly ?name cr =
(* used to add an hypothesis to the local hint database *)
let make_resolve_hyp env sigma decl =
- let hname = get_id decl in
+ let hname = NamedDecl.get_id decl in
try
[make_apply_entry env sigma (true, true, false) None false
~name:(PathHints [VarRef hname])
- (mkVar hname, get_type decl, Univ.ContextSet.empty)]
+ (mkVar hname, NamedDecl.get_type decl, Univ.ContextSet.empty)]
with
| Failure _ -> []
| e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 2b31695f62..72c3523da0 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -19,6 +19,8 @@ open Declarations
open Tacmach.New
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+
(* I implemented the following functions which test whether a term t
is an inductive but non-recursive type, a general conjuction, a
general disjunction, or a type with no constructors.
@@ -100,7 +102,7 @@ let match_with_one_constructor style onlybinary allow_rec t =
(decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in
if
List.for_all
- (fun decl -> let c = get_type decl in
+ (fun decl -> let c = RelDecl.get_type decl in
is_local_assum decl &&
isRel c &&
Int.equal (destRel c) mib.mind_nparams) ctx
@@ -109,7 +111,7 @@ let match_with_one_constructor style onlybinary allow_rec t =
else None
else
let ctyp = prod_applist mip.mind_nf_lc.(0) args in
- let cargs = List.map get_type (prod_assum ctyp) in
+ let cargs = List.map RelDecl.get_type (prod_assum ctyp) in
if not (is_lax_conjunction style) || has_nodep_prod ctyp then
(* Record or non strict conjunction *)
Some (hdapp,List.rev cargs)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 1a0bee0b89..291bc09650 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -28,7 +28,8 @@ open Misctypes
open Tacexpr
open Sigma.Notations
open Proofview.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
let var_occurs_in_pf gl id =
let env = Proofview.Goal.env gl in
@@ -182,7 +183,7 @@ let dependent_hyps env id idlist gl =
| [] -> []
| d::l ->
(* Update the type of id1: it may have been subject to rewriting *)
- let d = pf_get_hyp (get_id d) gl in
+ let d = pf_get_hyp (NamedDecl.get_id d) gl in
if occur_var_in_decl env id d
then d :: dep_rec l
else dep_rec l
@@ -192,7 +193,7 @@ let dependent_hyps env id idlist gl =
let split_dep_and_nodep hyps gl =
List.fold_right
(fun d (l1,l2) ->
- if var_occurs_in_pf gl (get_id d) then (d::l1,l2) else (l1,d::l2))
+ if var_occurs_in_pf gl (NamedDecl.get_id d) then (d::l1,l2) else (l1,d::l2))
hyps ([],[])
(* Computation of dids is late; must have been done in rewrite_equations*)
@@ -383,7 +384,7 @@ let rewrite_equations as_mode othin neqns names ba =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
let first_eq = ref MoveLast in
- let avoid = if as_mode then List.map get_id nodepids else [] in
+ let avoid = if as_mode then List.map NamedDecl.get_id nodepids else [] in
match othin with
| Some thin ->
tclTHENLIST
@@ -399,10 +400,10 @@ let rewrite_equations as_mode othin neqns names ba =
tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
names;
tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
- let idopt = if as_mode then Some (get_id d) else None in
+ let idopt = if as_mode then Some (NamedDecl.get_id d) else None in
intro_move idopt (if thin then MoveLast else !first_eq))
nodepids;
- (tclMAP (fun d -> tclTRY (clear [get_id d])) depids)]
+ (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)]
| None ->
(* simple inversion *)
if as_mode then
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 4f52df99c2..d80e862418 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -29,6 +29,8 @@ open Decl_kinds
open Proofview.Notations
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
let no_inductive_inconstr env sigma constr =
(str "Cannot recognize an inductive predicate in " ++
pr_lconstr_env env sigma constr ++
@@ -156,7 +158,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
let revargs,ownsign =
fold_named_context
(fun env d (revargs,hyps) ->
- let id = get_id d in
+ let id = NamedDecl.get_id d in
if Id.List.mem id ivars then
((mkVar id)::revargs, Context.Named.add d hyps)
else
@@ -206,7 +208,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let ownSign = ref begin
fold_named_context
(fun env d sign ->
- if mem_named_context (get_id d) global_named_context then sign
+ if mem_named_context (NamedDecl.get_id d) global_named_context then sign
else Context.Named.add d sign)
invEnv ~init:Context.Named.empty
end in
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
deleted file mode 100644
index 0110510d35..0000000000
--- a/tactics/taccoerce.ml
+++ /dev/null
@@ -1,344 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Util
-open Names
-open Term
-open Pattern
-open Misctypes
-open Genarg
-open Stdarg
-open Constrarg
-open Geninterp
-
-exception CannotCoerceTo of string
-
-let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
- let wit = Genarg.create_arg "constr_context" in
- let () = register_val0 wit None in
- wit
-
-(* includes idents known to be bound and references *)
-let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
- let wit = Genarg.create_arg "constr_under_binders" in
- let () = register_val0 wit None in
- wit
-
-(** All the types considered here are base types *)
-let val_tag wit = match val_tag wit with
-| Val.Base t -> t
-| _ -> assert false
-
-let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
- let Val.Dyn (t, _) = v in
- match Val.eq t (val_tag wit) with
- | None -> false
- | Some Refl -> true
-
-let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
- let Val.Dyn (t', x) = v in
- match Val.eq t t' with
- | None -> None
- | Some Refl -> Some x
-
-let in_gen wit v = Val.Dyn (val_tag wit, v)
-let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x
-
-module Value =
-struct
-
-type t = Val.t
-
-let normalize v = v
-
-let of_constr c = in_gen (topwit wit_constr) c
-
-let to_constr v =
- let v = normalize v in
- if has_type v (topwit wit_constr) then
- let c = out_gen (topwit wit_constr) v in
- Some c
- else if has_type v (topwit wit_constr_under_binders) then
- let vars, c = out_gen (topwit wit_constr_under_binders) v in
- match vars with [] -> Some c | _ -> None
- else None
-
-let of_uconstr c = in_gen (topwit wit_uconstr) c
-
-let to_uconstr v =
- let v = normalize v in
- if has_type v (topwit wit_uconstr) then
- Some (out_gen (topwit wit_uconstr) v)
- else None
-
-let of_int i = in_gen (topwit wit_int) i
-
-let to_int v =
- let v = normalize v in
- if has_type v (topwit wit_int) then
- Some (out_gen (topwit wit_int) v)
- else None
-
-let to_list v = prj Val.typ_list v
-
-let to_option v = prj Val.typ_opt v
-
-let to_pair v = prj Val.typ_pair v
-
-end
-
-let is_variable env id =
- Id.List.mem id (Termops.ids_of_named_context (Environ.named_context env))
-
-(* Transforms an id into a constr if possible, or fails with Not_found *)
-let constr_of_id env id =
- Term.mkVar (let _ = Environ.lookup_named id env in id)
-
-(* Gives the constr corresponding to a Constr_context tactic_arg *)
-let coerce_to_constr_context v =
- let v = Value.normalize v in
- if has_type v (topwit wit_constr_context) then
- out_gen (topwit wit_constr_context) v
- else raise (CannotCoerceTo "a term context")
-
-(* Interprets an identifier which must be fresh *)
-let coerce_var_to_ident fresh env v =
- let v = Value.normalize v in
- let fail () = raise (CannotCoerceTo "a fresh identifier") in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) -> id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
- out_gen (topwit wit_var) v
- else match Value.to_constr v with
- | None -> fail ()
- | Some c ->
- (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
- if isVar c && not (fresh && is_variable env (destVar c)) then
- destVar c
- else fail ()
-
-
-(* Interprets, if possible, a constr to an identifier which may not
- be fresh but suitable to be given to the fresh tactic. Works for
- vars, constants, inductive, constructors and sorts. *)
-let coerce_to_ident_not_fresh g env v =
-let id_of_name = function
- | Names.Anonymous -> Id.of_string "x"
- | Names.Name x -> x in
- let v = Value.normalize v in
- let fail () = raise (CannotCoerceTo "an identifier") in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) -> id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
- out_gen (topwit wit_var) v
- else
- match Value.to_constr v with
- | None -> fail ()
- | Some c ->
- match Constr.kind c with
- | Var id -> id
- | Meta m -> id_of_name (Evd.meta_name g m)
- | Evar (kn,_) ->
- begin match Evd.evar_ident kn g with
- | None -> fail ()
- | Some id -> id
- end
- | Const (cst,_) -> Label.to_id (Constant.label cst)
- | Construct (cstr,_) ->
- let ref = Globnames.ConstructRef cstr in
- let basename = Nametab.basename_of_global ref in
- basename
- | Ind (ind,_) ->
- let ref = Globnames.IndRef ind in
- let basename = Nametab.basename_of_global ref in
- basename
- | Sort s ->
- begin
- match s with
- | Prop _ -> Label.to_id (Label.make "Prop")
- | Type _ -> Label.to_id (Label.make "Type")
- end
- | _ -> fail()
-
-
-let coerce_to_intro_pattern env v =
- let v = Value.normalize v in
- if has_type v (topwit wit_intro_pattern) then
- snd (out_gen (topwit wit_intro_pattern) v)
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- IntroNaming (IntroIdentifier id)
- else match Value.to_constr v with
- | Some c when isVar c ->
- (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
- (* but also in "destruct H as (H,H')" *)
- IntroNaming (IntroIdentifier (destVar c))
- | _ -> raise (CannotCoerceTo "an introduction pattern")
-
-let coerce_to_intro_pattern_naming env v =
- match coerce_to_intro_pattern env v with
- | IntroNaming pat -> pat
- | _ -> raise (CannotCoerceTo "a naming introduction pattern")
-
-let coerce_to_hint_base v =
- let v = Value.normalize v in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) -> Id.to_string id
- | _ -> raise (CannotCoerceTo "a hint base name")
- else raise (CannotCoerceTo "a hint base name")
-
-let coerce_to_int v =
- let v = Value.normalize v in
- if has_type v (topwit wit_int) then
- out_gen (topwit wit_int) v
- else raise (CannotCoerceTo "an integer")
-
-let coerce_to_constr env v =
- let v = Value.normalize v in
- let fail () = raise (CannotCoerceTo "a term") in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) ->
- (try ([], constr_of_id env id) with Not_found -> fail ())
- | _ -> fail ()
- else if has_type v (topwit wit_constr) then
- let c = out_gen (topwit wit_constr) v in
- ([], c)
- else if has_type v (topwit wit_constr_under_binders) then
- out_gen (topwit wit_constr_under_binders) v
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- (try [], constr_of_id env id with Not_found -> fail ())
- else fail ()
-
-let coerce_to_uconstr env v =
- let v = Value.normalize v in
- if has_type v (topwit wit_uconstr) then
- out_gen (topwit wit_uconstr) v
- else
- raise (CannotCoerceTo "an untyped term")
-
-let coerce_to_closed_constr env v =
- let ids,c = coerce_to_constr env v in
- let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
- c
-
-let coerce_to_evaluable_ref env v =
- let fail () = raise (CannotCoerceTo "an evaluable reference") in
- let v = Value.normalize v in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
- else fail ()
- else if has_type v (topwit wit_ref) then
- let open Globnames in
- let r = out_gen (topwit wit_ref) v in
- match r with
- | VarRef var -> EvalVarRef var
- | ConstRef c -> EvalConstRef c
- | IndRef _ | ConstructRef _ -> fail ()
- else
- let ev = match Value.to_constr v with
- | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c))
- | Some c when isVar c -> EvalVarRef (destVar c)
- | _ -> fail ()
- in
- if Tacred.is_evaluable env ev then ev else fail ()
-
-let coerce_to_constr_list env v =
- let v = Value.to_list v in
- match v with
- | Some l ->
- let map v = coerce_to_closed_constr env v in
- List.map map l
- | None -> raise (CannotCoerceTo "a term list")
-
-let coerce_to_intro_pattern_list loc env v =
- match Value.to_list v with
- | None -> raise (CannotCoerceTo "an intro pattern list")
- | Some l ->
- let map v = (loc, coerce_to_intro_pattern env v) in
- List.map map l
-
-let coerce_to_hyp env v =
- let fail () = raise (CannotCoerceTo "a variable") in
- let v = Value.normalize v in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- if is_variable env id then id else fail ()
- else match Value.to_constr v with
- | Some c when isVar c -> destVar c
- | _ -> fail ()
-
-let coerce_to_hyp_list env v =
- let v = Value.to_list v in
- match v with
- | Some l ->
- let map n = coerce_to_hyp env n in
- List.map map l
- | None -> raise (CannotCoerceTo "a variable list")
-
-(* Interprets a qualified name *)
-let coerce_to_reference env v =
- let v = Value.normalize v in
- match Value.to_constr v with
- | Some c ->
- begin
- try Globnames.global_of_constr c
- with Not_found -> raise (CannotCoerceTo "a reference")
- end
- | None -> raise (CannotCoerceTo "a reference")
-
-(* Quantified named or numbered hypothesis or hypothesis in context *)
-(* (as in Inversion) *)
-let coerce_to_quantified_hypothesis v =
- let v = Value.normalize v in
- if has_type v (topwit wit_intro_pattern) then
- let v = out_gen (topwit wit_intro_pattern) v in
- match v with
- | _, IntroNaming (IntroIdentifier id) -> NamedHyp id
- | _ -> raise (CannotCoerceTo "a quantified hypothesis")
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- NamedHyp id
- else if has_type v (topwit wit_int) then
- AnonHyp (out_gen (topwit wit_int) v)
- else match Value.to_constr v with
- | Some c when isVar c -> NamedHyp (destVar c)
- | _ -> raise (CannotCoerceTo "a quantified hypothesis")
-
-(* Quantified named or numbered hypothesis or hypothesis in context *)
-(* (as in Inversion) *)
-let coerce_to_decl_or_quant_hyp env v =
- let v = Value.normalize v in
- if has_type v (topwit wit_int) then
- AnonHyp (out_gen (topwit wit_int) v)
- else
- try coerce_to_quantified_hypothesis v
- with CannotCoerceTo _ ->
- raise (CannotCoerceTo "a declared or quantified hypothesis")
-
-let coerce_to_int_or_var_list v =
- match Value.to_list v with
- | None -> raise (CannotCoerceTo "an int list")
- | Some l ->
- let map n = ArgArg (coerce_to_int n) in
- List.map map l
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
deleted file mode 100644
index 0b67f8726e..0000000000
--- a/tactics/taccoerce.mli
+++ /dev/null
@@ -1,96 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Util
-open Names
-open Term
-open Misctypes
-open Pattern
-open Genarg
-open Geninterp
-
-(** Coercions from highest level generic arguments to actual data used by Ltac
- interpretation. Those functions examinate dynamic types and try to return
- something sensible according to the object content. *)
-
-exception CannotCoerceTo of string
-(** Exception raised whenever a coercion failed. *)
-
-(** {5 High-level access to values}
-
- The [of_*] functions cast a given argument into a value. The [to_*] do the
- converse, and return [None] if there is a type mismatch.
-
-*)
-
-module Value :
-sig
- type t = Val.t
-
- val normalize : t -> t
- (** Eliminated the leading dynamic type casts. *)
-
- val of_constr : constr -> t
- val to_constr : t -> constr option
- val of_uconstr : Glob_term.closed_glob_constr -> t
- val to_uconstr : t -> Glob_term.closed_glob_constr option
- val of_int : int -> t
- val to_int : t -> int option
- val to_list : t -> t list option
- val to_option : t -> t option option
- val to_pair : t -> (t * t) option
-end
-
-(** {5 Coercion functions} *)
-
-val coerce_to_constr_context : Value.t -> constr
-
-val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t
-
-val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t
-
-val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
-
-val coerce_to_intro_pattern_naming :
- Environ.env -> Value.t -> intro_pattern_naming_expr
-
-val coerce_to_hint_base : Value.t -> string
-
-val coerce_to_int : Value.t -> int
-
-val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
-
-val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr
-
-val coerce_to_closed_constr : Environ.env -> Value.t -> constr
-
-val coerce_to_evaluable_ref :
- Environ.env -> Value.t -> evaluable_global_reference
-
-val coerce_to_constr_list : Environ.env -> Value.t -> constr list
-
-val coerce_to_intro_pattern_list :
- Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns
-
-val coerce_to_hyp : Environ.env -> Value.t -> Id.t
-
-val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list
-
-val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference
-
-val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis
-
-val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis
-
-val coerce_to_int_or_var_list : Value.t -> int or_var list
-
-(** {5 Missing generic arguments} *)
-
-val wit_constr_context : (Empty.t, Empty.t, constr) genarg_type
-
-val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type
diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml
index 4d4ca7d9ef..ef45ee47e1 100644
--- a/tactics/tactic_matching.ml
+++ b/tactics/tactic_matching.ml
@@ -13,6 +13,8 @@ open Names
open Tacexpr
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
(** [t] is the type of matching successes. It ultimately contains a
{!Tacexpr.glob_tactic_expr} representing the left-hand side of the
corresponding matching rule, a matching substitution to be
@@ -280,9 +282,9 @@ module PatternMatching (E:StaticEnvironment) = struct
the name of the matched hypothesis. *)
let hyp_match_type hypname pat hyps =
pick hyps >>= fun decl ->
- let id = get_id decl in
+ let id = NamedDecl.get_id decl in
let refresh = is_local_def decl in
- pattern_match_term refresh pat (get_type decl) () <*>
+ pattern_match_term refresh pat (NamedDecl.get_type decl) () <*>
put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
return id
@@ -319,7 +321,7 @@ module PatternMatching (E:StaticEnvironment) = struct
(* spiwack: alternatively it is possible to return the list
with the matched hypothesis removed directly in
[hyp_match]. *)
- let select_matched_hyp decl = Id.equal (get_id decl) matched_hyp in
+ let select_matched_hyp decl = Id.equal (NamedDecl.get_id decl) matched_hyp in
let hyps = CList.remove_first select_matched_hyp hyps in
hyp_pattern_list_match pats hyps lhs
| [] -> return lhs
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9c2dd3fee1..203d975428 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -16,7 +16,8 @@ open Declarations
open Tacmach
open Clenv
open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
(************************************************************************)
(* Tacticals re-exported from the Refiner module *)
@@ -70,7 +71,7 @@ let nthDecl m gl =
try List.nth (pf_hyps gl) (m-1)
with Failure _ -> error "No such assumption."
-let nthHypId m gl = nthDecl m gl |> get_id
+let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id
let nthHyp m gl = mkVar (nthHypId m gl)
let lastDecl gl = nthDecl 1 gl
@@ -81,7 +82,7 @@ let nLastDecls n gl =
try List.firstn n (pf_hyps gl)
with Failure _ -> error "Not enough hypotheses in the goal."
-let nLastHypsId n gl = List.map get_id (nLastDecls n gl)
+let nLastHypsId n gl = List.map NamedDecl.get_id (nLastDecls n gl)
let nLastHyps n gl = List.map mkVar (nLastHypsId n gl)
let onNthDecl m tac gl = tac (nthDecl m gl) gl
@@ -99,7 +100,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac
let onNLastHyps n tac = onHyps (nLastHyps n) tac
let afterHyp id gl =
- fst (List.split_when (Id.equal id % get_id) (pf_hyps gl))
+ fst (List.split_when (NamedDecl.get_id %> Id.equal id) (pf_hyps gl))
(***************************************)
(* Clause Tacticals *)
@@ -560,7 +561,7 @@ module New = struct
let nthHypId m gl =
(** We only use [id] *)
let gl = Proofview.Goal.assume gl in
- nthDecl m gl |> get_id
+ nthDecl m gl |> NamedDecl.get_id
let nthHyp m gl =
mkVar (nthHypId m gl)
@@ -592,7 +593,7 @@ module New = struct
let afterHyp id tac =
Proofview.Goal.enter { enter = begin fun gl ->
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
- let rem, _ = List.split_when (Id.equal id % get_id) hyps in
+ let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in
tac rem
end }
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 96dc8a2e2c..85b6e8de9e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,6 +43,10 @@ open Locusops
open Misctypes
open Proofview.Notations
open Sigma.Notations
+open Context.Named.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
let inj_with_occurrences e = (AllOccurrences,e)
@@ -162,19 +166,17 @@ let _ =
(** This tactic creates a partial proof realizing the introduction rule, but
does not check anything. *)
let unsafe_intro env store decl b =
- let open Context.Named.Declaration in
Refine.refine ~unsafe:true { run = begin fun sigma ->
let ctx = named_context_val env in
let nctx = push_named_context_val decl ctx in
- let inst = List.map (mkVar % get_id) (named_context env) in
+ let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
let ninst = mkRel 1 :: inst in
- let nb = subst1 (mkVar (get_id decl)) b in
+ let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
Sigma (mkNamedLambda_or_LetIn decl ev, sigma, p)
end }
let introduction ?(check=true) id =
- let open Context.Named.Declaration in
Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
let concl = Proofview.Goal.concl gl in
@@ -186,6 +188,7 @@ let introduction ?(check=true) id =
user_err ~hdr:"Tactics.introduction"
(str "Variable " ++ pr_id id ++ str " is already declared.")
in
+ let open Context.Named.Declaration in
match kind_of_term (whd_evar sigma concl) with
| Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
| LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
@@ -317,7 +320,6 @@ let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest)
(* Renaming hypotheses *)
let rename_hyp repl =
- let open Context.Named.Declaration in
let fold accu (src, dst) = match accu with
| None -> None
| Some (srcs, dsts) ->
@@ -339,7 +341,7 @@ let rename_hyp repl =
let concl = Proofview.Goal.concl gl in
let store = Proofview.Goal.extra gl in
(** Check that we do not mess variables *)
- let fold accu decl = Id.Set.add (get_id decl) accu in
+ let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in
let vars = List.fold_left fold Id.Set.empty hyps in
let () =
if not (Id.Set.subset src vars) then
@@ -358,13 +360,13 @@ let rename_hyp repl =
let subst = List.map make_subst repl in
let subst c = Vars.replace_vars subst c in
let map decl =
- decl |> map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id)
- |> map_constr subst
+ decl |> NamedDecl.map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id)
+ |> NamedDecl.map_constr subst
in
let nhyps = List.map map hyps in
let nconcl = subst concl in
let nctx = Environ.val_of_named_context nhyps in
- let instance = List.map (mkVar % get_id) hyps in
+ let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
Refine.refine ~unsafe:true { run = begin fun sigma ->
Evarutil.new_evar_instance nctx sigma nconcl ~store instance
end }
@@ -869,14 +871,17 @@ let reduction_clause redexp cl =
(None, bind_red_expr_occurrences occs nbcl redexp)) cl
let reduce redexp cl =
+ let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in
+ Proofview.Trace.name_tactic trace begin
Proofview.Goal.enter { enter = begin fun gl ->
- let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
- let redexps = reduction_clause redexp cl in
+ let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
+ let redexps = reduction_clause redexp cl' in
let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
Tacticals.New.tclMAP (fun (where,redexp) ->
e_reduct_option ~check
(Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps
end }
+ end
(* Unfolding occurrences of a constant *)
@@ -982,23 +987,21 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
aux n []
let get_next_hyp_position id gl =
- let open Context.Named.Declaration in
let rec aux = function
| [] -> raise (RefinerError (NoSuchHyp id))
| decl :: right ->
- if Id.equal (get_id decl) id then
- match right with decl::_ -> MoveBefore (get_id decl) | [] -> MoveLast
+ if Id.equal (NamedDecl.get_id decl) id then
+ match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveLast
else
aux right
in
aux (Proofview.Goal.hyps (Proofview.Goal.assume gl))
let get_previous_hyp_position id gl =
- let open Context.Named.Declaration in
let rec aux dest = function
| [] -> raise (RefinerError (NoSuchHyp id))
| decl :: right ->
- let hyp = get_id decl in
+ let hyp = NamedDecl.get_id decl in
if Id.equal hyp id then dest else aux (MoveAfter hyp) right
in
aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
@@ -1270,7 +1273,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
let naming = NamingMustBe (dloc,targetid) in
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
- (Proofview.Unsafe.tclEVARS clenv.evd)
+ (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
(if sidecond_first then
Tacticals.New.tclTHENFIRST
(assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac
@@ -1559,7 +1562,7 @@ let make_projection env sigma params cstr sign elim i n c u =
| NotADefinedRecordUseScheme elim ->
(* bugs: goes from right to left when i increases! *)
let decl = List.nth cstr.cs_args i in
- let t = get_type decl in
+ let t = RelDecl.get_type decl in
let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> b in
let branch = it_mkLambda_or_LetIn b cstr.cs_args in
if
@@ -1943,7 +1946,6 @@ let exact_proof c =
end }
let assumption =
- let open Context.Named.Declaration in
let rec arec gl only_eq = function
| [] ->
if only_eq then
@@ -1951,7 +1953,7 @@ let assumption =
arec gl false hyps
else Tacticals.New.tclZEROMSG (str "No such assumption.")
| decl::rest ->
- let t = get_type decl in
+ let t = NamedDecl.get_type decl in
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
let (sigma, is_same_type) =
@@ -1962,7 +1964,7 @@ let assumption =
in
if is_same_type then
(Proofview.Unsafe.tclEVARS sigma) <*>
- Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h }
+ Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (NamedDecl.get_id decl)) h }
else arec gl only_eq rest
in
let assumption_tac = { enter = begin fun gl ->
@@ -1992,7 +1994,7 @@ let check_is_type env sigma ty =
let check_decl env sigma decl =
let open Context.Named.Declaration in
- let ty = get_type decl in
+ let ty = NamedDecl.get_type decl in
let evdref = ref sigma in
try
let _ = Typing.e_sort_of env evdref ty in
@@ -2002,7 +2004,7 @@ let check_decl env sigma decl =
in
!evdref
with e when CErrors.noncritical e ->
- let id = get_id decl in
+ let id = NamedDecl.get_id decl in
raise (DependsOnBody (Some id))
let clear_body ids =
@@ -2034,7 +2036,7 @@ let clear_body ids =
check_decl env sigma decl
else sigma
in
- let seen = seen || List.mem_f Id.equal (get_id decl) ids in
+ let seen = seen || List.mem_f Id.equal (NamedDecl.get_id decl) ids in
(push_named decl env, sigma, seen)
in
let (env, sigma, _) = List.fold_left check (base_env, sigma, false) (List.rev ctx) in
@@ -2074,13 +2076,12 @@ let rec intros_clearing = function
(* Keeping only a few hypotheses *)
let keep hyps =
- let open Context.Named.Declaration in
Proofview.Goal.nf_enter { enter = begin fun gl ->
Proofview.tclENV >>= fun env ->
let ccl = Proofview.Goal.concl gl in
let cl,_ =
fold_named_context_reverse (fun (clear,keep) decl ->
- let hyp = get_id decl in
+ let hyp = NamedDecl.get_id decl in
if Id.List.mem hyp hyps
|| List.exists (occur_var_in_decl env hyp) keep
|| occur_var env hyp ccl
@@ -2618,13 +2619,12 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
end }
let insert_before decls lasthyp env =
- let open Context.Named.Declaration in
match lasthyp with
| None -> push_named_context decls env
| Some id ->
Environ.fold_named_context
(fun _ d env ->
- let env = if Id.equal id (get_id d) then push_named_context decls env else env in
+ let env = if Id.equal id (NamedDecl.get_id d) then push_named_context decls env else env in
push_named d env)
~init:(reset_context env) env
@@ -2763,19 +2763,18 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
generalize_goal_gen env sigma ids i o t cl
let old_generalize_dep ?(with_let=false) c gl =
- let open Context.Named.Declaration in
let env = pf_env gl in
let sign = pf_hyps gl in
let init_ids = ids_of_named_context (Global.named_context()) in
let seek (d:Context.Named.Declaration.t) (toquant:Context.Named.t) =
- if List.exists (fun d' -> occur_var_in_decl env (get_id d') d) toquant
+ if List.exists (fun d' -> occur_var_in_decl env (NamedDecl.get_id d') d) toquant
|| dependent_in_decl c d then
d::toquant
else
toquant in
let to_quantify = Context.Named.fold_outside seek sign ~init:[] in
let to_quantify_rev = List.rev to_quantify in
- let qhyps = List.map get_id to_quantify_rev in
+ let qhyps = List.map NamedDecl.get_id to_quantify_rev in
let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
let tothin' =
match kind_of_term c with
@@ -2787,7 +2786,7 @@ let old_generalize_dep ?(with_let=false) c gl =
let body =
if with_let then
match kind_of_term c with
- | Var id -> Tacmach.pf_get_hyp gl id |> get_value
+ | Var id -> id |> Tacmach.pf_get_hyp gl |> NamedDecl.get_value
| _ -> None
else None
in
@@ -2936,7 +2935,7 @@ let unfold_body x =
| LocalDef (_,xval,_) -> xval
in
Tacticals.New.afterHyp x begin fun aft ->
- let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in
+ let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in
let rfun _ _ c = replace_vars [x, xval] c in
let reducth h = reduct_in_hyp rfun h in
let reductc = reduct_in_concl (rfun, DEFAULTcast) in
@@ -3255,7 +3254,6 @@ exception Shunt of Id.t move_location
let cook_sign hyp0_opt inhyps indvars env =
(* First phase from L to R: get [toclear], [decldep] and [statuslist]
for the hypotheses before (= more ancient than) hyp0 (see above) *)
- let open Context.Named.Declaration in
let toclear = ref [] in
let avoid = ref [] in
let decldeps = ref [] in
@@ -3265,7 +3263,7 @@ let cook_sign hyp0_opt inhyps indvars env =
let before = ref true in
let maindep = ref false in
let seek_deps env decl rhyp =
- let hyp = get_id decl in
+ let hyp = NamedDecl.get_id decl in
if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false)
then begin
before:=false;
@@ -3284,7 +3282,7 @@ let cook_sign hyp0_opt inhyps indvars env =
in
let depother = List.is_empty inhyps &&
(List.exists (fun id -> occur_var_in_decl env id decl) indvars ||
- List.exists (fun decl' -> occur_var_in_decl env (get_id decl') decl) !decldeps)
+ List.exists (fun decl' -> occur_var_in_decl env (NamedDecl.get_id decl') decl) !decldeps)
in
if not (List.is_empty inhyps) && Id.List.mem hyp inhyps
|| dephyp0 || depother
@@ -3307,7 +3305,7 @@ let cook_sign hyp0_opt inhyps indvars env =
let _ = fold_named_context seek_deps env ~init:MoveFirst in
(* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *)
let compute_lstatus lhyp decl =
- let hyp = get_id decl in
+ let hyp = NamedDecl.get_id decl in
if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false) then
raise (Shunt lhyp);
if Id.List.mem hyp !ldeps then begin
@@ -3475,8 +3473,8 @@ let ids_of_constr ?(all=false) vars c =
Array.fold_left_from
(if all then 0 else mib.Declarations.mind_nparams)
aux vars args
- | _ -> fold_constr aux vars c)
- | _ -> fold_constr aux vars c
+ | _ -> Term.fold_constr aux vars c)
+ | _ -> Term.fold_constr aux vars c
in aux vars c
let decompose_indapp f args =
@@ -3531,13 +3529,12 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
end }
let hyps_of_vars env sign nogen hyps =
- let open Context.Named.Declaration in
if Id.Set.is_empty hyps then []
else
let (_,lh) =
Context.Named.fold_inside
(fun (hs,hl) d ->
- let x = get_id d in
+ let x = NamedDecl.get_id d in
if Id.Set.mem x nogen then (hs,hl)
else if Id.Set.mem x hs then (hs,x::hl)
else
@@ -3567,8 +3564,7 @@ let linear vars args =
with Seen -> false
let is_defined_variable env id =
- let open Context.Named.Declaration in
- lookup_named id env |> is_local_def
+ env |> lookup_named id |> is_local_def
let abstract_args gl generalize_vars dep id defined f args =
let open Context.Rel.Declaration in
@@ -3591,7 +3587,7 @@ let abstract_args gl generalize_vars dep id defined f args =
let name, ty, arity =
let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
let decl = List.hd rel in
- get_name decl, get_type decl, c
+ RelDecl.get_name decl, RelDecl.get_type decl, c
in
let argty = Tacmach.pf_unsafe_type_of gl arg in
let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
@@ -4026,14 +4022,15 @@ let is_functional_induction elimc gl =
need a dependent one or not *)
let get_eliminator elim dep s gl =
- let open Context.Rel.Declaration in
match elim with
| ElimUsing (elim,indsign) ->
Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign
| ElimOver (isrec,id) ->
let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
let _, (l, s) = compute_elim_signature elims id in
- let branchlengthes = List.map (fun d -> assert (is_local_assum d); pi1 (decompose_prod_letin (get_type d))) (List.rev s.branches) in
+ let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (RelDecl.get_type d)))
+ (List.rev s.branches)
+ in
evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l
(* Instantiate all meta variables of elimclause using lid, some elts
@@ -4095,7 +4092,6 @@ let induction_tac with_evars params indvars elim =
induction applies with the induction hypotheses *)
let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_tac =
- let open Context.Named.Declaration in
Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
@@ -4108,7 +4104,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
let s = Retyping.get_sort_family_of env sigma tmpcl in
let deps_cstr =
List.fold_left
- (fun a decl -> if is_local_assum decl then (mkVar (get_id decl))::a else a) [] deps in
+ (fun a decl -> if NamedDecl.is_local_assum decl then (mkVar (NamedDecl.get_id decl))::a else a) [] deps in
let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in
let branchletsigns =
let f (_,is_not_let,_,_) = is_not_let in
@@ -4190,7 +4186,6 @@ let induction_without_atomization isrec with_evars elim names lid =
(* assume that no occurrences are selected *)
let clear_unselected_context id inhyps cls =
Proofview.Goal.nf_enter { enter = begin fun gl ->
- let open Context.Named.Declaration in
if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) &&
cls.concl_occs == NoOccurrences
then user_err
@@ -4199,7 +4194,7 @@ let clear_unselected_context id inhyps cls =
match cls.onhyps with
| Some hyps ->
let to_erase d =
- let id' = get_id d in
+ let id' = NamedDecl.get_id d in
if Id.List.mem id' inhyps then (* if selected, do not erase *) None
else
(* erase if not selected and dependent on id or selected hyps *)
@@ -4766,7 +4761,7 @@ let interpretable_as_section_decl evd d1 d2 =
| LocalDef _, LocalAssum _ -> false
| LocalDef (_,b1,t1), LocalDef (_,b2,t2) ->
e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2
- | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (get_type d2)
+ | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2)
let rec decompose len c t accu =
let open Context.Rel.Declaration in
@@ -4779,7 +4774,6 @@ let rec decompose len c t accu =
| _ -> assert false
let rec shrink ctx sign c t accu =
- let open Context.Rel.Declaration in
match ctx, sign with
| [], [] -> (c, t, accu)
| p :: ctx, decl :: sign ->
@@ -4790,9 +4784,9 @@ let rec shrink ctx sign c t accu =
else
let c = mkLambda_or_LetIn p c in
let t = mkProd_or_LetIn p t in
- let accu = if is_local_assum p then let open Context.Named.Declaration in
- mkVar (get_id decl) :: accu
- else accu
+ let accu = if RelDecl.is_local_assum p
+ then mkVar (NamedDecl.get_id decl) :: accu
+ else accu
in
shrink ctx sign c t accu
| _ -> assert false
@@ -4818,7 +4812,6 @@ let abstract_subproof id gk tac =
let open Tacticals.New in
let open Tacmach.New in
let open Proofview.Notations in
- let open Context.Named.Declaration in
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let current_sign = Global.named_context()
@@ -4828,7 +4821,7 @@ let abstract_subproof id gk tac =
let sign,secsign =
List.fold_right
(fun d (s1,s2) ->
- let id = get_id d in
+ let id = NamedDecl.get_id d in
if mem_named_context id current_sign &&
interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d
then (s1,push_named_context_val d s2)
@@ -4865,8 +4858,13 @@ let abstract_subproof id gk tac =
in
let cd = Entries.DefinitionEntry const in
let decl = (cd, IsProof Lemma) in
- (** ppedrot: seems legit to have abstracted subproofs as local*)
- let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in
+ let cst () =
+ (** do not compute the implicit arguments, it may be costly *)
+ let () = Impargs.make_implicit_args false in
+ (** ppedrot: seems legit to have abstracted subproofs as local*)
+ Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl
+ in
+ let cst = Impargs.with_implicit_protection cst () in
(* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
let evd = Evd.set_universe_context evd ectx in
@@ -4950,7 +4948,7 @@ module New = struct
let reduce_after_refine =
reduce
(Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]})
- {onhyps=None; concl_occs=AllOccurrences }
+ {onhyps=Some []; concl_occs=AllOccurrences }
let refine ?unsafe c =
Refine.refine ?unsafe c <*>
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 48722f655a..093302608e 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -12,7 +12,6 @@ Equality
Contradiction
Inv
Leminv
-Taccoerce
Hints
Auto
Eauto
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 03:31:10 +0000