aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/glob_term_to_relation.ml8
-rw-r--r--plugins/ltac/evar_tactics.ml2
-rw-r--r--plugins/ltac/extraargs.ml475
-rw-r--r--plugins/ltac/extraargs.mli5
-rw-r--r--plugins/ltac/extratactics.ml416
-rw-r--r--plugins/ltac/tacinterp.ml14
-rw-r--r--plugins/omega/PreOmega.v4
-rw-r--r--plugins/ssr/ssrfwd.ml4
-rw-r--r--plugins/ssr/ssrtacticals.ml4
9 files changed, 19 insertions, 113 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index bbc0a37c69..fd2d90e9cf 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1469,7 +1469,7 @@ let do_build_inductive
(rel_constructors)
in
let rel_ind i ext_rel_constructors =
- (((CAst.make @@ relnames.(i)), None),
+ ((CAst.make @@ relnames.(i)),
rel_params,
Some rel_arities.(i),
ext_rel_constructors),[]
@@ -1499,14 +1499,14 @@ let do_build_inductive
let _time2 = System.get_time () in
try
with_full_print
- (Flags.silently (ComInductive.do_mutual_inductive ~template:None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
+ (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
Declarations.Finite
with
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
let repacked_rel_inds =
- List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+ List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
rel_inds
in
let msg =
@@ -1521,7 +1521,7 @@ let do_build_inductive
let _time3 = System.get_time () in
(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
let repacked_rel_inds =
- List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+ List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
rel_inds
in
let msg =
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 84f13d2131..73490a2dfd 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -94,7 +94,7 @@ let let_evar name typ =
in
let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere)
+ (Tactics.pose_tac (Name.Name id) evar)
end
let hget_evar n =
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 38600695dc..f4555509cc 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -311,78 +311,3 @@ let pr_lpar_id_colon _ _ _ _ = mt ()
ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
| [ local_test_lpar_id_colon(x) ] -> [ () ]
END
-
-(* spiwack: the print functions are incomplete, but I don't know what they are
- used for *)
-let pr_r_int31_field i31f =
- str "int31 " ++
- match i31f with
- | Retroknowledge.Int31Bits -> str "bits"
- | Retroknowledge.Int31Type -> str "type"
- | Retroknowledge.Int31Twice -> str "twice"
- | Retroknowledge.Int31TwicePlusOne -> str "twice plus one"
- | Retroknowledge.Int31Phi -> str "phi"
- | Retroknowledge.Int31PhiInv -> str "phi inv"
- | Retroknowledge.Int31Plus -> str "plus"
- | Retroknowledge.Int31Times -> str "times"
- | Retroknowledge.Int31Constructor -> assert false
- | Retroknowledge.Int31PlusC -> str "plusc"
- | Retroknowledge.Int31PlusCarryC -> str "pluscarryc"
- | Retroknowledge.Int31Minus -> str "minus"
- | Retroknowledge.Int31MinusC -> str "minusc"
- | Retroknowledge.Int31MinusCarryC -> str "minuscarryc"
- | Retroknowledge.Int31TimesC -> str "timesc"
- | Retroknowledge.Int31Div21 -> str "div21"
- | Retroknowledge.Int31Div -> str "div"
- | Retroknowledge.Int31Diveucl -> str "diveucl"
- | Retroknowledge.Int31AddMulDiv -> str "addmuldiv"
- | Retroknowledge.Int31Compare -> str "compare"
- | Retroknowledge.Int31Head0 -> str "head0"
- | Retroknowledge.Int31Tail0 -> str "tail0"
- | Retroknowledge.Int31Lor -> str "lor"
- | Retroknowledge.Int31Land -> str "land"
- | Retroknowledge.Int31Lxor -> str "lxor"
-
-let pr_retroknowledge_field f =
- match f with
- (* | Retroknowledge.KEq -> str "equality"
- | Retroknowledge.KNat natf -> pr_r_nat_field () () () natf
- | Retroknowledge.KN nf -> pr_r_n_field () () () nf *)
- | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++
- spc () ++ str "in " ++ qs group
-
-VERNAC ARGUMENT EXTEND retroknowledge_int31
-PRINTED BY pr_r_int31_field
-| [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
-| [ "int31" "type" ] -> [ Retroknowledge.Int31Type ]
-| [ "int31" "twice" ] -> [ Retroknowledge.Int31Twice ]
-| [ "int31" "twice" "plus" "one" ] -> [ Retroknowledge.Int31TwicePlusOne ]
-| [ "int31" "phi" ] -> [ Retroknowledge.Int31Phi ]
-| [ "int31" "phi" "inv" ] -> [ Retroknowledge.Int31PhiInv ]
-| [ "int31" "plus" ] -> [ Retroknowledge.Int31Plus ]
-| [ "int31" "plusc" ] -> [ Retroknowledge.Int31PlusC ]
-| [ "int31" "pluscarryc" ] -> [ Retroknowledge.Int31PlusCarryC ]
-| [ "int31" "minus" ] -> [ Retroknowledge.Int31Minus ]
-| [ "int31" "minusc" ] -> [ Retroknowledge.Int31MinusC ]
-| [ "int31" "minuscarryc" ] -> [ Retroknowledge.Int31MinusCarryC ]
-| [ "int31" "times" ] -> [ Retroknowledge.Int31Times ]
-| [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ]
-| [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ]
-| [ "int31" "div" ] -> [ Retroknowledge.Int31Div ]
-| [ "int31" "diveucl" ] -> [ Retroknowledge.Int31Diveucl ]
-| [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ]
-| [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ]
-| [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ]
-| [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ]
-| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ]
-| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ]
-| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ]
-END
-
-VERNAC ARGUMENT EXTEND retroknowledge_field
-PRINTED BY pr_retroknowledge_field
-(*| [ "equality" ] -> [ Retroknowledge.KEq ]
-| [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ]
-| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]*)
-| [ retroknowledge_int31 (i) "in" string(g)] -> [ Retroknowledge.KInt31(g,i) ]
-END
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e477b12cd3..fa70235975 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -72,11 +72,6 @@ val test_lpar_id_colon : unit Pcoq.Entry.t
val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
-(** Spiwack: Primitive for retroknowledge registration *)
-
-val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t
-val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
-
val wit_in_clause :
(lident Locus.clause_expr,
lident Locus.clause_expr,
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index dc027c4041..8dad6260ae 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -545,22 +545,6 @@ END
(**********************************************************************)
-(*spiwack : Vernac commands for retroknowledge *)
-
-VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
- | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
- [ let env = Global.env () in
- let evd = Evd.from_env env in
- let tc,_ctx = Constrintern.interp_constr env evd c in
- let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in
- let tc = EConstr.to_constr evd tc in
- let tb = EConstr.to_constr evd tb in
- Global.register f tc tb ]
-END
-
-
-
-(**********************************************************************)
(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
defined by Conor McBride *)
TACTIC EXTEND generalize_eqs
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f4313a8fa3..71da6c7667 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1664,16 +1664,18 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* We try to fully-typecheck the term *)
let flags = open_constr_use_classes_flags () in
let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in
- let let_tac b na c cl eqpat =
- let id = Option.default (make IntroAnonymous) eqpat in
- let with_eq = if b then None else Some (true,id) in
- Tactics.letin_tac with_eq na c None cl
- in
let na = interp_name ist env sigma na in
+ let let_tac =
+ if b then Tactics.pose_tac na c_interp
+ else
+ let id = Option.default (make IntroAnonymous) eqpat in
+ let with_eq = Some (true, id) in
+ Tactics.letin_tac with_eq na c_interp None Locusops.nowhere
+ in
Tacticals.New.tclWITHHOLES ev
(name_atomic ~env
(TacLetTac(ev,na,c_interp,clp,b,eqpat))
- (let_tac b na c_interp clp eqpat)) sigma
+ let_tac) sigma
else
(* We try to keep the pattern structure as much as possible *)
let let_pat_tac b na c cl eqpat =
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 59fd9b8017..094adfda7a 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -85,6 +85,7 @@ Ltac zify_binop t thm a b:=
Ltac zify_op_1 :=
match goal with
+ | x := ?t : Z |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
| |- context [ Z.max ?a ?b ] => zify_binop Z.max Z.max_spec a b
| H : context [ Z.max ?a ?b ] |- _ => zify_binop Z.max Z.max_spec a b
| |- context [ Z.min ?a ?b ] => zify_binop Z.min Z.min_spec a b
@@ -114,6 +115,7 @@ Ltac hide_Z_of_nat t :=
Ltac zify_nat_rel :=
match goal with
(* I: equalities *)
+ | x := ?t : nat |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
| |- (@eq nat ?a ?b) => apply (Nat2Z.inj a b) (* shortcut *)
| H : context [ @eq nat ?a ?b ] |- _ => rewrite <- (Nat2Z.inj_iff a b) in H
| |- context [ @eq nat ?a ?b ] => rewrite <- (Nat2Z.inj_iff a b)
@@ -223,6 +225,7 @@ Ltac hide_Zpos t :=
Ltac zify_positive_rel :=
match goal with
(* I: equalities *)
+ | x := ?t : positive |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
| |- (@eq positive ?a ?b) => apply Pos2Z.inj
| H : context [ @eq positive ?a ?b ] |- _ => rewrite <- (Pos2Z.inj_iff a b) in H
| |- context [ @eq positive ?a ?b ] => rewrite <- (Pos2Z.inj_iff a b)
@@ -348,6 +351,7 @@ Ltac hide_Z_of_N t :=
Ltac zify_N_rel :=
match goal with
(* I: equalities *)
+ | x := ?t : N |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
| |- (@eq N ?a ?b) => apply (N2Z.inj a b) (* shortcut *)
| H : context [ @eq N ?a ?b ] |- _ => rewrite <- (N2Z.inj_iff a b) in H
| |- context [ @eq N ?a ?b ] => rewrite <- (N2Z.inj_iff a b)
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index e367cd32d6..f67cf20e49 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -25,9 +25,7 @@ module RelDecl = Context.Rel.Declaration
(** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *)
(** Defined identifier *)
-
-let settac id c = Tactics.letin_tac None (Name id) c None
-let posetac id cl = Proofview.V82.of_tactic (settac id cl Locusops.nowhere)
+let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl)
let ssrposetac (id, (_, t)) gl =
let ist, t =
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 83581f3416..f12f9fac0f 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -14,7 +14,6 @@ open Names
open Constr
open Termops
open Tacmach
-open Locusops
open Ssrast
open Ssrcommon
@@ -82,8 +81,7 @@ let pf_clauseids gl gens clseq =
let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false
-let settac id c = Tactics.letin_tac None (Name id) c None
-let posetac id cl = Proofview.V82.of_tactic (settac id cl nowhere)
+let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl)
let hidetacs clseq idhide cl0 =
if not (hidden_clseq clseq) then [] else
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:57:41 +0000