aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/hints.ml8
-rw-r--r--tactics/hipattern.ml14
-rw-r--r--tactics/leminv.ml6
-rw-r--r--tactics/leminv.mli2
-rw-r--r--tactics/tactics.ml72
5 files changed, 54 insertions, 48 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml
index a572508d47..3ccbab874f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -56,7 +56,9 @@ let head_constr_bound sigma t =
| _ -> raise Bound
let head_constr sigma c =
- try head_constr_bound sigma c with Bound -> user_err Pp.(str "Bound head variable.")
+ try head_constr_bound sigma c
+ with Bound -> user_err (Pp.str "Head identifier must be a constant, section variable, \
+ (co)inductive type, (co)inductive type constructor, or projection.")
let decompose_app_bound sigma t =
let t = strip_outer_cast sigma t in
@@ -764,7 +766,9 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with
let try_head_pattern c =
try head_pattern_bound c
- with BoundPattern -> user_err Pp.(str "Bound head variable.")
+ with BoundPattern ->
+ user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \
+ an if, case, or let expression, an application, or a projection.")
let with_uid c = { obj = c; uid = fresh_key () }
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index b057cf72bc..75fae6647d 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -252,16 +252,16 @@ open Decl_kinds
open Evar_kinds
let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
-let mkGApp f args = CAst.make @@ GApp (f, args)
-let mkGHole = CAst.make @@
+let mkGApp f args = DAst.make @@ GApp (f, args)
+let mkGHole = DAst.make @@
GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None)
-let mkGProd id c1 c2 = CAst.make @@
+let mkGProd id c1 c2 = DAst.make @@
GProd (Name (Id.of_string id), Explicit, c1, c2)
-let mkGArrow c1 c2 = CAst.make @@
+let mkGArrow c1 c2 = DAst.make @@
GProd (Anonymous, Explicit, c1, c2)
-let mkGVar id = CAst.make @@ GVar (Id.of_string id)
-let mkGPatVar id = CAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id))
-let mkGRef r = CAst.make @@ GRef (Lazy.force r, None)
+let mkGVar id = DAst.make @@ GVar (Id.of_string id)
+let mkGPatVar id = DAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id))
+let mkGRef r = DAst.make @@ GRef (Lazy.force r, None)
let mkGAppRef r args = mkGApp (mkGRef r) args
(** forall x : _, _ x x *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index aeb80ae57c..7c488f524f 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,7 +232,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
let invProof = EConstr.Unsafe.to_constr invProof in
let p = Evarutil.nf_evars_universes sigma invProof in
- p, Evd.universe_context sigma
+ p, Evd.universe_context ~names:[] ~extensible:true sigma
let add_inversion_lemma name env sigma t sort dep inv_op =
let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
@@ -248,9 +248,9 @@ let add_inversion_lemma_exn na com comsort bool tac =
let env = Global.env () in
let evd = ref (Evd.from_env env) in
let c = Constrintern.interp_type_evars env evd com in
- let sigma, sort = Pretyping.interp_sort !evd comsort in
+ let evd, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env !evd comsort in
try
- add_inversion_lemma na env sigma c sort bool tac
+ add_inversion_lemma na env evd c sort bool tac
with
| UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
user_err ~hdr:"Inv needs Nodep Prop Set" s
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 41b0e09b42..8745ad3979 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -15,5 +15,5 @@ val lemInv_clause :
quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
val add_inversion_lemma_exn :
- Id.t -> constr_expr -> glob_sort -> bool -> (Id.t -> unit Proofview.tactic) ->
+ Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
unit
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 67bc55d3fe..f1dd61358c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -74,7 +74,7 @@ let _ =
let _ =
declare_bool_option
- { optdepr = false;
+ { optdepr = true; (* remove in 8.8 *)
optname = "trigger bugged context matching compatibility";
optkey = ["Tactic";"Compat";"Context"];
optread = (fun () -> !Flags.tactic_context_compat) ;
@@ -2219,27 +2219,27 @@ let check_number_of_constructors expctdnumopt i nconstr =
end;
if i > nconstr then error "Not enough constructors."
-let constructor_tac with_evars expctdnumopt i lbind =
+let constructor_core with_evars cstr lbind =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let (sigma, (cons, u)) = Evd.fresh_constructor_instance env sigma cstr in
+ let cons = mkConstructU (cons, EInstance.make u) in
+ let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in
+ Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) apply_tac
+ end
+
+let constructor_tac with_evars expctdnumopt i lbind =
+ Proofview.Goal.enter begin fun gl ->
let cl = Tacmach.New.pf_concl gl in
- let reduce_to_quantified_ind =
- Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
- in
- let (mind,redcl) = reduce_to_quantified_ind cl in
- let nconstr =
- Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
- check_number_of_constructors expctdnumopt i nconstr;
-
- let (sigma, (cons, u)) = Evd.fresh_constructor_instance
- (Proofview.Goal.env gl) sigma (fst mind, i) in
- let cons = mkConstructU (cons, EInstance.make u) in
-
- let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in
- Tacticals.New.tclTHENLIST
- [ Proofview.Unsafe.tclEVARS sigma;
- convert_concl_no_check redcl DEFAULTcast;
- intros; apply_tac]
+ let ((ind,_),redcl) = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl cl in
+ let nconstr = Array.length (snd (Global.lookup_inductive ind)).mind_consnames in
+ check_number_of_constructors expctdnumopt i nconstr;
+ Tacticals.New.tclTHENLIST [
+ convert_concl_no_check redcl DEFAULTcast;
+ intros;
+ constructor_core with_evars (ind, i) lbind
+ ]
end
let one_constructor i lbind = constructor_tac false None i lbind
@@ -2249,24 +2249,26 @@ let one_constructor i lbind = constructor_tac false None i lbind
Should be generalize in Constructor (Fun c : I -> tactic)
*)
-let rec tclANY tac = function
-| [] -> Tacticals.New.tclZEROMSG (str "No applicable tactic.")
-| arg :: l ->
- Tacticals.New.tclORD (tac arg) (fun () -> tclANY tac l)
-
let any_constructor with_evars tacopt =
- let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
- let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in
+ let one_constr =
+ let tac cstr = constructor_core with_evars cstr NoBindings in
+ match tacopt with
+ | None -> tac
+ | Some t -> fun cstr -> Tacticals.New.tclTHEN (tac cstr) t in
+ let rec any_constr ind n i () =
+ if Int.equal i n then one_constr (ind,i)
+ else Tacticals.New.tclORD (one_constr (ind,i)) (any_constr ind n (i + 1)) in
Proofview.Goal.enter begin fun gl ->
let cl = Tacmach.New.pf_concl gl in
- let reduce_to_quantified_ind =
- Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
- in
- let mind = fst (reduce_to_quantified_ind cl) in
+ let (ind,_),redcl = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl cl in
let nconstr =
- Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
+ Array.length (snd (Global.lookup_inductive ind)).mind_consnames in
if Int.equal nconstr 0 then error "The type has no constructors.";
- tclANY tac (List.interval 1 nconstr)
+ Tacticals.New.tclTHENLIST [
+ convert_concl_no_check redcl DEFAULTcast;
+ intros;
+ any_constr ind nconstr 1 ()
+ ]
end
let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1
@@ -4131,7 +4133,7 @@ let guess_elim isrec dep s hyp0 gl =
let env = Tacmach.New.pf_env gl in
let sigma = Tacmach.New.project gl in
let u = EInstance.kind (Tacmach.New.project gl) u in
- if use_dependent_propositions_elimination () && dep
+ if use_dependent_propositions_elimination () && dep = Some true
then
let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in
let ind = EConstr.of_constr ind in
@@ -4165,7 +4167,7 @@ let find_induction_type isrec elim hyp0 gl =
| None ->
let sort = Tacticals.New.elimination_sort_of_goal gl in
let _, (elimc,elimt),_ =
- guess_elim isrec (* dummy: *) true sort hyp0 gl in
+ guess_elim isrec None sort hyp0 gl in
let scheme = compute_elim_sig sigma ~elimc elimt in
(* We drop the scheme waiting to know if it is dependent *)
scheme, ElimOver (isrec,hyp0)
@@ -4199,7 +4201,7 @@ let get_eliminator elim dep s gl =
| 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 evd, (elimc,elimt),_ as elims = guess_elim isrec (Some dep) s id gl in
let _, (l, s) = compute_elim_signature elims id in
let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d)))
(List.rev s.branches)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 16:27:54 +0000