aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/abstract.ml6
-rw-r--r--tactics/elimschemes.ml12
-rw-r--r--tactics/elimschemes.mli1
-rw-r--r--tactics/equality.ml55
-rw-r--r--tactics/tacticals.ml8
-rw-r--r--tactics/tacticals.mli9
6 files changed, 42 insertions, 49 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index a5b2f99457..e91fe5067c 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -103,8 +103,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
question, how does abstract behave when discharge is local for example?
*)
let goal_kind, suffix = if opaque
- then (Global,poly,Proof Theorem), "_subproof"
- else (Global,poly,DefinitionBody Definition), "_subterm" in
+ then (Global ImportDefaultBehavior,poly,Proof Theorem), "_subproof"
+ else (Global ImportDefaultBehavior,poly,DefinitionBody Definition), "_subterm" in
let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
(* 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_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:true id decl
+ Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl
in
let cst, eff = Impargs.with_implicit_protection cst () in
let inst = match const.Entries.const_entry_universes with
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 1170c1acd0..8ead050262 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -59,7 +59,7 @@ let build_induction_scheme_in_type dep sort ind =
let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
let sigma, c = build_induction_scheme env sigma pind dep sort in
c, Evd.evar_universe_context sigma
-
+
let rect_scheme_kind_from_type =
declare_individual_scheme_object "_rect_nodep"
(fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
@@ -108,6 +108,16 @@ let sind_scheme_kind_from_prop =
declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop"
(fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants)
+let nondep_elim_scheme from_kind to_kind =
+ match from_kind, to_kind with
+ | InProp, InProp -> ind_scheme_kind_from_prop
+ | InProp, InSProp -> sind_scheme_kind_from_prop
+ | InProp, InSet -> rec_scheme_kind_from_prop
+ | InProp, InType -> rect_scheme_kind_from_prop
+ | _ , InProp -> ind_scheme_kind_from_type
+ | _ , InSProp -> sind_scheme_kind_from_type
+ | _ , InSet -> rec_scheme_kind_from_type
+ | _ , InType -> rect_scheme_kind_from_type
(* Case analysis *)
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 4472792449..f60e6c137a 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -33,6 +33,7 @@ val sind_dep_scheme_kind_from_type : individual scheme_kind
val rec_scheme_kind_from_type : individual scheme_kind
val rec_dep_scheme_kind_from_type : individual scheme_kind
+val nondep_elim_scheme : Sorts.family -> Sorts.family -> individual scheme_kind
(** Case analysis schemes *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 51eee2a053..ec0876110b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -352,35 +352,35 @@ let find_elim hdcncl lft2rgt dep cls ot =
(is_global_exists "core.JMeq.type" hdcncl
&& jmeq_same_dom env sigma ot)) && not dep
then
- let c =
+ let c =
match EConstr.kind sigma hdcncl with
- | Ind (ind_sp,u) ->
- let pr1 =
+ | Ind (ind_sp,u) ->
+ let pr1 =
lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl)
- in
+ in
begin match lft2rgt, cls with
| Some true, None
| Some false, Some _ ->
- let c1 = destConstRef pr1 in
+ let c1 = destConstRef pr1 in
let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
- let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in
+ let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in
let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
- begin
- try
- let _ = Global.lookup_constant c1' in
- c1'
- with Not_found ->
+ begin
+ try
+ let _ = Global.lookup_constant c1' in
+ c1'
+ with Not_found ->
user_err ~hdr:"Equality.find_elim"
(str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
end
- | _ -> destConstRef pr1
+ | _ -> destConstRef pr1
end
| _ ->
(* cannot occur since we checked that we are in presence of
Logic.eq or Jmeq just before *)
assert false
in
- pf_constr_of_global (ConstRef c)
+ pf_constr_of_global (ConstRef c)
else
let scheme_name = match dep, lft2rgt, inccl with
(* Non dependent case *)
@@ -946,12 +946,12 @@ let build_coq_I () = pf_constr_of_global (lib_ref "core.True.I")
let rec build_discriminator env sigma true_0 false_0 dirn c = function
| [] ->
let ind = get_type_of env sigma c in
- build_selector env sigma dirn c ind true_0 false_0
+ build_selector env sigma dirn c ind true_0 (fst false_0)
| ((sp,cnum),argnum)::l ->
let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
let newc = mkRel(cnum_nlams-argnum) in
let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in
- kont sigma subval (false_0,mkProp)
+ kont sigma subval false_0
(* Note: discrimination could be more clever: if some elimination is
not allowed because of a large impredicative constructor in the
@@ -983,25 +983,22 @@ let gen_absurdity id =
absurd_term=False
*)
-let ind_scheme_of_eq lbeq =
+let ind_scheme_of_eq lbeq to_kind =
let (mib,mip) = Global.lookup_inductive (destIndRef lbeq.eq) in
- let kind = inductive_sort_family mip in
+ let from_kind = inductive_sort_family mip in
(* use ind rather than case by compatibility *)
- let kind =
- if kind == InProp then Elimschemes.ind_scheme_kind_from_prop
- else Elimschemes.ind_scheme_kind_from_type in
+ let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in
let c, eff = find_scheme kind (destIndRef lbeq.eq) in
ConstRef c, eff
-let discrimination_pf e (t,t1,t2) discriminator lbeq =
+let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind =
build_coq_I () >>= fun i ->
- build_coq_False () >>= fun absurd_term ->
- let eq_elim, eff = ind_scheme_of_eq lbeq in
+ let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in
Proofview.tclEFFECTS eff <*>
pf_constr_of_global eq_elim >>= fun eq_elim ->
Proofview.tclUNIT
- (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]), absurd_term)
+ (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]))
let eq_baseid = Id.of_string "e"
@@ -1018,21 +1015,23 @@ let apply_on_clause (f,t) clause =
let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
build_coq_True () >>= fun true_0 ->
build_coq_False () >>= fun false_0 ->
+ let false_ty = Retyping.get_type_of env sigma false_0 in
+ let false_kind = Retyping.get_sort_family_of env sigma false_0 in
let e = next_ident_away eq_baseid (vars_of_env env) in
let e_env = push_named (Context.Named.Declaration.LocalAssum (make_annot e Sorts.Relevant,t)) env in
let discriminator =
try
Proofview.tclUNIT
- (build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath)
+ (build_discriminator e_env sigma true_0 (false_0,false_ty) dirn (mkVar e) cpath)
with
UserError _ as ex -> Proofview.tclZERO ex
in
discriminator >>= fun discriminator ->
- discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) ->
- let pf_ty = mkArrow eqn Sorts.Relevant absurd_term in
+ discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf ->
+ let pf_ty = mkArrow eqn Sorts.Relevant false_0 in
let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
- tclTHENS (assert_after Anonymous absurd_term)
+ tclTHENS (assert_after Anonymous false_0)
[onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))]
let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 59fd8b37d6..81700986ea 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -43,12 +43,8 @@ let tclTHENS = Refiner.tclTHENS
let tclTHENSV = Refiner.tclTHENSV
let tclTHENSFIRSTn = Refiner.tclTHENSFIRSTn
let tclTHENSLASTn = Refiner.tclTHENSLASTn
-let tclTHENFIRSTn = Refiner.tclTHENFIRSTn
-let tclTHENLASTn = Refiner.tclTHENLASTn
let tclREPEAT = Refiner.tclREPEAT
-let tclREPEAT_MAIN = Refiner.tclREPEAT_MAIN
let tclFIRST = Refiner.tclFIRST
-let tclSOLVE = Refiner.tclSOLVE
let tclTRY = Refiner.tclTRY
let tclCOMPLETE = Refiner.tclCOMPLETE
let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
@@ -58,10 +54,6 @@ let tclDO = Refiner.tclDO
let tclPROGRESS = Refiner.tclPROGRESS
let tclSHOWHYPS = Refiner.tclSHOWHYPS
let tclTHENTRY = Refiner.tclTHENTRY
-let tclIFTHENELSE = Refiner.tclIFTHENELSE
-let tclIFTHENSELSE = Refiner.tclIFTHENSELSE
-let tclIFTHENSVELSE = Refiner.tclIFTHENSVELSE
-let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST
(************************************************************************)
(* Tacticals applying on hypotheses *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 201b7801c3..a9ccda527f 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -31,13 +31,9 @@ val tclTHENLAST : tactic -> tactic -> tactic
val tclTHENS : tactic -> tactic list -> tactic
val tclTHENSV : tactic -> tactic array -> tactic
val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
-val tclTHENLASTn : tactic -> tactic array -> tactic
val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
-val tclTHENFIRSTn : tactic -> tactic array -> tactic
val tclREPEAT : tactic -> tactic
-val tclREPEAT_MAIN : tactic -> tactic
val tclFIRST : tactic list -> tactic
-val tclSOLVE : tactic list -> tactic
val tclTRY : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
@@ -49,11 +45,6 @@ val tclSHOWHYPS : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclMAP : ('a -> tactic) -> 'a list -> tactic
-val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
-val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic
-val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic
-val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
-
(** {6 Tacticals applying to hypotheses } *)
val onNthHypId : int -> (Id.t -> tactic) -> tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 07:02:54 +0000