aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/plugin_base.dune1
-rw-r--r--plugins/ltac/rewrite.ml16
-rw-r--r--plugins/ltac/tacenv.ml7
-rw-r--r--plugins/ltac/tacintern.ml13
-rw-r--r--plugins/ltac/tacinterp.ml9
5 files changed, 21 insertions, 25 deletions
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
index 5611f5ba16..1b31655310 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/plugin_base.dune
@@ -3,6 +3,7 @@
(public_name coq.plugins.ltac)
(synopsis "Coq's LTAC tactic language")
(modules :standard \ tauto)
+ (flags :standard -open Gramlib)
(libraries coq.stm))
(library
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9dd98a4ab7..9f7669f1d5 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -89,8 +89,8 @@ let goalevars evars = fst evars
let cstrevars evars = snd evars
let new_cstr_evar (evd,cstrs) env t =
- let s = Typeclasses.set_resolvable Evd.Store.empty false in
- let (evd', t) = Evarutil.new_evar ~store:s env evd t in
+ (** We handle the typeclass resolution of constraints ourselves *)
+ let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in
let ev, _ = destEvar evd' t in
(evd', Evar.Set.add ev cstrs), t
@@ -632,9 +632,6 @@ let solve_remaining_by env sigma holes by =
let no_constraints cstrs =
fun ev _ -> not (Evar.Set.mem ev cstrs)
-let all_constraints cstrs =
- fun ev _ -> Evar.Set.mem ev cstrs
-
let poly_inverse sort =
if sort then PropGlobal.inverse else TypeGlobal.inverse
@@ -1453,10 +1450,11 @@ let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars =
res
let solve_constraints env (evars,cstrs) =
- let filter = all_constraints cstrs in
- Typeclasses.resolve_typeclasses env ~filter ~split:false ~fail:true
- (Typeclasses.mark_resolvables ~filter evars)
-
+ let oldtcs = Evd.get_typeclass_evars evars in
+ let evars' = Evd.set_typeclass_evars evars cstrs in
+ let evars' = Typeclasses.resolve_typeclasses env ~filter:all_evars ~split:false ~fail:true evars' in
+ Evd.set_typeclass_evars evars' oldtcs
+
let nf_zeta =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 1f2c722b34..a88285c9ee 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -115,7 +115,6 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
(* Summary and Object declaration *)
-open Nametab
open Libobject
type ltac_entry = {
@@ -153,19 +152,19 @@ let tac_deprecation kn =
let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
| None ->
- let () = if not local then push_tactic (Until i) sp kn in
+ let () = if not local then push_tactic (Nametab.Until i) sp kn in
add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
| None ->
- let () = if not local then push_tactic (Exactly i) sp kn in
+ let () = if not local then push_tactic (Nametab.Exactly i) sp kn in
add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with
| None ->
- let () = push_tactic (Until 1) sp kn in
+ let () = push_tactic (Nametab.Until 1) sp kn in
add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 5501cf92a5..55412c74bb 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -19,7 +19,6 @@ open Util
open Names
open Libnames
open Globnames
-open Nametab
open Smartlocate
open Constrexpr
open Termops
@@ -98,7 +97,7 @@ let intern_global_reference ist qid =
ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
else
try ArgArg (qid.CAst.loc,locate_global_with_alias qid)
- with Not_found -> error_global_not_found qid
+ with Not_found -> Nametab.error_global_not_found qid
let intern_ltac_variable ist qid =
if qualid_is_ident qid && find_var (qualid_basename qid) ist then
@@ -150,7 +149,7 @@ let intern_isolated_tactic_reference strict ist qid =
try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid))
with Not_found ->
(* Reference not found *)
- error_global_not_found qid
+ Nametab.error_global_not_found qid
(* Internalize an applied tactic reference *)
@@ -169,7 +168,7 @@ let intern_applied_tactic_reference ist qid =
try intern_applied_global_tactic_reference qid
with Not_found ->
(* Reference not found *)
- error_global_not_found qid
+ Nametab.error_global_not_found qid
(* Intern a reference parsed in a non-tactic entry *)
@@ -190,7 +189,7 @@ let intern_non_tactic_reference strict ist qid =
TacGeneric ipat
else
(* Reference not found *)
- error_global_not_found qid
+ Nametab.error_global_not_found qid
let intern_message_token ist = function
| (MsgString _ | MsgInt _ as x) -> x
@@ -302,7 +301,7 @@ let intern_evaluable_global_reference ist qid =
try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid)
with Not_found ->
if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid)
- else error_global_not_found qid
+ else Nametab.error_global_not_found qid
let intern_evaluable_reference_or_by_notation ist = function
| {v=AN r} -> intern_evaluable_global_reference ist r
@@ -377,7 +376,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
subterm matched when a pattern *)
let r = match r with
| {v=AN r} -> r
- | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in
+ | {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (smart_global r))) in
let sign = {
Constrintern.ltac_vars = ist.ltacvars;
ltac_bound = Id.Set.empty;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f90e889678..b60b77595b 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -23,7 +23,6 @@ open Names
open Nameops
open Libnames
open Globnames
-open Nametab
open Refiner
open Tacmach.New
open Tactic_debug
@@ -358,7 +357,7 @@ let interp_reference ist env sigma = function
with Not_found ->
try
VarRef (get_id (Environ.lookup_named id env))
- with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
+ with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
let try_interp_evaluable env (loc, id) =
let v = Environ.lookup_named id env in
@@ -374,14 +373,14 @@ let interp_evaluable ist env sigma = function
with Not_found ->
match r with
| EvalConstRef _ -> r
- | _ -> error_global_not_found (qualid_of_ident ?loc id)
+ | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
end
| ArgArg (r,None) -> r
| ArgVar {loc;v=id} ->
try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
try try_interp_evaluable env (loc, id)
- with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
+ with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
(* Interprets an hypothesis name *)
let interp_occurrences ist occs =
@@ -640,7 +639,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
(try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
- error_global_not_found (qualid_of_ident ?loc id))
+ Nametab.error_global_not_found (qualid_of_ident ?loc id))
| Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
| Inr c -> Inr (interp_typed_pattern ist env sigma c) in
interp_occurrences ist occs, p
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 05:05:11 +0000