aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml47
-rw-r--r--plugins/ltac/rewrite.ml44
-rw-r--r--plugins/ltac/tacentries.ml48
-rw-r--r--plugins/ltac/tacentries.mli5
4 files changed, 42 insertions, 62 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index ba3fa6fa0d..e5b032e638 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -693,12 +693,7 @@ let rewrite_except h =
end
-let refl_equal =
- let coq_base_constant s =
- Coqlib.gen_reference_in_modules "RecursiveDefinition"
- (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in
- function () -> (coq_base_constant "eq_refl")
-
+let refl_equal () = Coqlib.lib_ref "core.eq.type"
(* This is simply an implementation of the case_eq tactic. this code
should be replaced by a call to the tactic but I don't know how to
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 5b8bd6d01a..9dd98a4ab7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -56,12 +56,14 @@ let init_setoid () =
if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
+let find_reference dir s =
+ Coqlib.find_reference "generalized rewriting" dir s
+[@@warning "-3"]
+
let lazy_find_reference dir s =
- let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in
+ let gr = lazy (find_reference dir s) in
fun () -> Lazy.force gr
-let find_reference dir s = Coqlib.coq_reference "generalized rewriting" dir s
-
type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
let find_global dir s =
@@ -74,13 +76,13 @@ let find_global dir s =
(** Global constants. *)
-let coq_eq_ref = lazy_find_reference ["Init"; "Logic"] "eq"
-let coq_eq = find_global ["Init"; "Logic"] "eq"
-let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
-let coq_all = find_global ["Init"; "Logic"] "all"
-let impl = find_global ["Program"; "Basics"] "impl"
+let coq_eq_ref () = Coqlib.lib_ref "core.eq.type"
+let coq_eq = find_global ["Coq"; "Init"; "Logic"] "eq"
+let coq_f_equal = find_global ["Coq"; "Init"; "Logic"] "f_equal"
+let coq_all = find_global ["Coq"; "Init"; "Logic"] "all"
+let impl = find_global ["Coq"; "Program"; "Basics"] "impl"
-(** Bookkeeping which evars are constraints so that we can
+(** Bookkeeping which evars are constraints so that we can
remove them at the end of the tactic. *)
let goalevars evars = fst evars
@@ -154,7 +156,7 @@ end) = struct
let respectful = find_global morphisms "respectful"
let respectful_ref = lazy_find_reference morphisms "respectful"
- let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation"
+ let default_relation = find_global ["Coq"; "Classes"; "SetoidTactics"] "DefaultRelation"
let coq_forall = find_global morphisms "forall_def"
@@ -374,12 +376,12 @@ let type_app_poly env env evd f args =
module PropGlobal = struct
module Consts =
struct
- let relation_classes = ["Classes"; "RelationClasses"]
- let morphisms = ["Classes"; "Morphisms"]
- let relation = ["Relations";"Relation_Definitions"], "relation"
+ let relation_classes = ["Coq"; "Classes"; "RelationClasses"]
+ let morphisms = ["Coq"; "Classes"; "Morphisms"]
+ let relation = ["Coq"; "Relations";"Relation_Definitions"], "relation"
let app_poly = app_poly_nocheck
- let arrow = find_global ["Program"; "Basics"] "arrow"
- let coq_inverse = find_global ["Program"; "Basics"] "flip"
+ let arrow = find_global ["Coq"; "Program"; "Basics"] "arrow"
+ let coq_inverse = find_global ["Coq"; "Program"; "Basics"] "flip"
end
module G = GlobalBindings(Consts)
@@ -395,12 +397,12 @@ end
module TypeGlobal = struct
module Consts =
struct
- let relation_classes = ["Classes"; "CRelationClasses"]
- let morphisms = ["Classes"; "CMorphisms"]
+ let relation_classes = ["Coq"; "Classes"; "CRelationClasses"]
+ let morphisms = ["Coq"; "Classes"; "CMorphisms"]
let relation = relation_classes, "crelation"
let app_poly = app_poly_check
- let arrow = find_global ["Classes"; "CRelationClasses"] "arrow"
- let coq_inverse = find_global ["Classes"; "CRelationClasses"] "flip"
+ let arrow = find_global ["Coq"; "Classes"; "CRelationClasses"] "arrow"
+ let coq_inverse = find_global ["Coq"; "Classes"; "CRelationClasses"] "flip"
end
module G = GlobalBindings(Consts)
@@ -740,9 +742,9 @@ let new_global (evars, cstrs) gr =
(sigma, cstrs), c
let make_eq sigma =
- new_global sigma (Coqlib.build_coq_eq ())
+ new_global sigma Coqlib.(lib_ref "core.eq.type")
let make_eq_refl sigma =
- new_global sigma (Coqlib.build_coq_eq_refl ())
+ new_global sigma Coqlib.(lib_ref "core.eq.refl")
let get_rew_prf evars r = match r.rew_prf with
| RewPrf (rel, prf) -> evars, (rel, prf)
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 636cb8ebf8..a77a9c2f45 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -187,7 +187,7 @@ let add_tactic_entry (kn, ml, tg) state =
| TacTerm s -> GramTerminal s
| TacNonTerm (loc, (s, ido)) ->
let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
- GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, e))
+ GramNonTerminal (Loc.tag ?loc @@ (typ, e))
in
let prods = List.map map tg.tacgram_prods in
let rules = make_rule mkact prods in
@@ -556,18 +556,14 @@ let () =
] in
register_grammars_by_name "tactic" entries
-let get_identifier id =
+let get_identifier i =
(** Workaround for badly-designed generic arguments lacking a closure *)
- Names.Id.of_string_soft ("$" ^ id)
-
+ Names.Id.of_string_soft (Printf.sprintf "$%i" i)
type _ ty_sig =
| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
| TyIdent : string * 'r ty_sig -> 'r ty_sig
-| TyArg :
- ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig
-| TyAnonArg :
- ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig
+| TyArg : ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> ('c -> 'r) ty_sig
type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
@@ -581,18 +577,16 @@ let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.a
| TUentry a -> Uentry (Genarg.ArgT.Any a)
| TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i)
-let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list =
- fun sign -> match sign with
+let rec clause_of_sign : type a. int -> a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list =
+ fun i sign -> match sign with
| TyNil -> []
- | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig'
- | TyArg (a, id, sig') ->
- let id = get_identifier id in
- TacNonTerm (None,(untype_user_symbol a,Some id)) :: clause_of_sign sig'
- | TyAnonArg (a, sig') ->
- TacNonTerm (None,(untype_user_symbol a,None)) :: clause_of_sign sig'
+ | TyIdent (s, sig') -> TacTerm s :: clause_of_sign i sig'
+ | TyArg (a, sig') ->
+ let id = Some (get_identifier i) in
+ TacNonTerm (None, (untype_user_symbol a, id)) :: clause_of_sign (i + 1) sig'
let clause_of_ty_ml = function
- | TyML (t,_) -> clause_of_sign t
+ | TyML (t,_) -> clause_of_sign 1 t
let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
fun sign tac ->
@@ -603,7 +597,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
| _ :: _ -> assert false
end
| TyIdent (s, sig') -> eval_sign sig' tac
- | TyArg (a, _, sig') ->
+ | TyArg (a, sig') ->
let f = eval_sign sig' in
begin fun tac vals ist -> match vals with
| [] -> assert false
@@ -611,7 +605,6 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol a)) v in
f (tac v') vals ist
end tac
- | TyAnonArg (a, sig') -> eval_sign sig' tac
let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function
| TyML (t,tac) -> eval_sign t tac
@@ -623,14 +616,12 @@ let is_constr_entry = function
let rec only_constr : type a. a ty_sig -> bool = function
| TyNil -> true
| TyIdent(_,_) -> false
-| TyArg (u, _, s) -> if is_constr_entry u then only_constr s else false
-| TyAnonArg (u, s) -> if is_constr_entry u then only_constr s else false
+| TyArg (u, s) -> if is_constr_entry u then only_constr s else false
-let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function
+let rec mk_sign_vars : type a. int -> a ty_sig -> Name.t list = fun i tu -> match tu with
| TyNil -> []
-| TyIdent (_,s) -> mk_sign_vars s
-| TyArg (_, name, s) -> Name (get_identifier name) :: mk_sign_vars s
-| TyAnonArg (_, s) -> Anonymous :: mk_sign_vars s
+| TyIdent (_,s) -> mk_sign_vars i s
+| TyArg (_, s) -> Name (get_identifier i) :: mk_sign_vars (i + 1) s
let dummy_id = Id.of_string "_"
@@ -661,12 +652,7 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
| [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s ->
(** The extension is only made of a name followed by constr entries: we do not
add any grammar nor printing rule and add it as a true Ltac definition. *)
- (*
- let patt = make_patt rem in
- let vars = List.map make_var rem in
- let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in
- *)
- let vars = mk_sign_vars s in
+ let vars = mk_sign_vars 1 s in
let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in
let tac = match s with
| TyNil -> eval ml_tac
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 138a584e01..0b2b426018 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -73,10 +73,7 @@ val print_located_tactic : Libnames.qualid -> unit
type _ ty_sig =
| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
| TyIdent : string * 'r ty_sig -> 'r ty_sig
-| TyArg :
- ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig
-| TyAnonArg :
- ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig
+| TyArg : ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> ('c -> 'r) ty_sig
type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 04:33:33 +0000