aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml46
-rw-r--r--plugins/ltac/g_class.ml42
-rw-r--r--plugins/ltac/g_ltac.ml410
-rw-r--r--plugins/ltac/pptactic.ml12
-rw-r--r--plugins/ltac/rewrite.ml8
-rw-r--r--plugins/ltac/rewrite.mli2
-rw-r--r--plugins/ltac/taccoerce.ml6
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml7
-rw-r--r--plugins/ltac/tacinterp.ml8
10 files changed, 33 insertions, 30 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 65c186a419..4b1555e551 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -415,7 +415,7 @@ VERNAC COMMAND EXTEND DeriveInversionClear
-> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
- -> [ add_inversion_lemma_exn na c InProp false inv_clear_tac ]
+ -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ]
END
VERNAC COMMAND EXTEND DeriveInversion
@@ -424,7 +424,7 @@ VERNAC COMMAND EXTEND DeriveInversion
-> [ add_inversion_lemma_exn na c s false inv_tac ]
| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
- -> [ add_inversion_lemma_exn na c InProp false inv_tac ]
+ -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ]
END
VERNAC COMMAND EXTEND DeriveDependentInversion
@@ -514,7 +514,7 @@ let cache_transitivity_lemma (_,(left,lem)) =
let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
-let inTransitivity : bool * Term.constr -> obj =
+let inTransitivity : bool * Constr.t -> obj =
declare_object {(default_object "TRANSITIVITY-STEPS") with
cache_function = cache_transitivity_lemma;
open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o);
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 104977aef3..ed2d9da63a 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -91,7 +91,7 @@ END
(** TODO: DEPRECATE *)
(* A progress test that allows to see if the evars have changed *)
-open Term
+open Constr
open Proofview.Notations
let rec eq_constr_mod_evars sigma x y =
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index c577cb2198..1161525689 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -232,10 +232,12 @@ GEXTEND Gram
| l = ident -> Name.Name l ] ]
;
let_clause:
- [ [ id = identref; ":="; te = tactic_expr ->
- (id, arg_of_expr te)
- | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
- (id, arg_of_expr (TacFun(args,te))) ] ]
+ [ [ (l,id) = identref; ":="; te = tactic_expr ->
+ ((l,Name id), arg_of_expr te)
+ | na = ["_" -> (Some !@loc,Anonymous)]; ":="; te = tactic_expr ->
+ (na, arg_of_expr te)
+ | (l,id) = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
+ ((l,Name id), arg_of_expr (TacFun(args,te))) ] ]
;
match_pattern:
[ [ IDENT "context"; oid = OPT Constr.ident;
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e467d3e2ca..38460c669f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -536,8 +536,8 @@ let pr_goal_selector ~toplevel s =
let pr_funvar n = spc () ++ Name.print n
- let pr_let_clause k pr (id,(bl,t)) =
- hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
+ let pr_let_clause k pr (na,(bl,t)) =
+ hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++
str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t)))
let pr_let_clauses recflag pr = function
@@ -1120,10 +1120,10 @@ let pr_goal_selector ~toplevel s =
let ty = EConstr.Unsafe.to_constr ty in
let rec strip_ty acc n ty =
if n=0 then (List.rev acc, EConstr.of_constr ty) else
- match Term.kind_of_term ty with
- Term.Prod(na,a,b) ->
- strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
- | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
+ match Constr.kind ty with
+ | Constr.Prod(na,a,b) ->
+ strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let pr_atomic_tactic_level env sigma n t =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1809f0fcdb..705a51edd3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -12,7 +12,7 @@ open CErrors
open Util
open Nameops
open Namegen
-open Term
+open Constr
open EConstr
open Vars
open Reduction
@@ -426,7 +426,7 @@ let split_head = function
| [] -> assert(false)
let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') =
- pb == pb' || (ty == ty' && Term.eq_constr x x' && Term.eq_constr y y')
+ pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y')
let problem_inclusion x y =
List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
@@ -928,8 +928,8 @@ let fold_match ?(force=false) env sigma c =
it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
in
let sk =
- if sortp == InProp then
- if sortc == InProp then
+ if sortp == Sorts.InProp then
+ if sortc == Sorts.InProp then
if dep then case_dep_scheme_kind_from_prop
else case_scheme_kind_from_prop
else (
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 63e891b455..1306c590ba 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -37,7 +37,7 @@ type ('constr,'redexpr) strategy_ast =
type rewrite_proof =
| RewPrf of constr * constr
- | RewCast of Term.cast_kind
+ | RewCast of Constr.cast_kind
type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4d171ecbc2..c03a867326 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -8,7 +8,7 @@
open Util
open Names
-open Term
+open Constr
open EConstr
open Misctypes
open Genarg
@@ -172,8 +172,8 @@ let id_of_name = function
| Sort s ->
begin
match ESorts.kind sigma s with
- | Prop _ -> Label.to_id (Label.make "Prop")
- | Type _ -> Label.to_id (Label.make "Type")
+ | Sorts.Prop _ -> Label.to_id (Label.make "Prop")
+ | Sorts.Type _ -> Label.to_id (Label.make "Type")
end
| _ -> fail()
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 1639736883..9bd3efc6b7 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -254,7 +254,7 @@ and 'a gen_tactic_expr =
| TacFail of global_flag * int or_var * 'n message_token list
| TacInfo of 'a gen_tactic_expr
| TacLetIn of rec_flag *
- (Id.t located * 'a gen_tactic_arg) list *
+ (Name.t located * 'a gen_tactic_arg) list *
'a gen_tactic_expr
| TacMatch of lazy_flag *
'a gen_tactic_expr *
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index f171fd07d7..b16b0a7bae 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -468,9 +468,10 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
(* Utilities *)
let extract_let_names lrc =
let fold accu ((loc, name), _) =
- if Id.Set.mem name accu then user_err ?loc
+ Nameops.Name.fold_right (fun id accu ->
+ if Id.Set.mem id accu then user_err ?loc
~hdr:"glob_tactic" (str "This variable is bound several times.")
- else Id.Set.add name accu
+ else Id.Set.add id accu) name accu
in
List.fold_left fold Id.Set.empty lrc
@@ -812,7 +813,7 @@ let notation_subst bindings tac =
let fold id c accu =
let loc = Glob_ops.loc_of_glob_constr (fst c) in
let c = ConstrMayEval (ConstrTerm c) in
- ((loc, id), c) :: accu
+ ((loc, Name id), c) :: accu
in
let bindings = Id.Map.fold fold bindings [] in
(** This is theoretically not correct due to potential variable capture, but
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fd75862c6f..1a8ec6d6f6 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1397,9 +1397,9 @@ and tactic_of_value ist vle =
and interp_letrec ist llc u =
Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *)
let lref = ref ist.lfun in
- let fold accu ((_, id), b) =
+ let fold accu ((_, na), b) =
let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in
- Id.Map.add id v accu
+ Name.fold_right (fun id -> Id.Map.add id v) na accu
in
let lfun = List.fold_left fold ist.lfun llc in
let () = lref := lfun in
@@ -1412,9 +1412,9 @@ and interp_letin ist llc u =
| [] ->
let ist = { ist with lfun } in
val_interp ist u
- | ((_, id), body) :: defs ->
+ | ((_, na), body) :: defs ->
Ftactic.bind (interp_tacarg ist body) (fun v ->
- fold (Id.Map.add id v lfun) defs)
+ fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs)
in
fold ist.lfun llc
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 12:56:58 +0000