aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/g_tactic.mlg10
-rw-r--r--plugins/ltac/rewrite.ml19
-rw-r--r--plugins/micromega/persistent_cache.ml29
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
4 files changed, 30 insertions, 30 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 236de65462..072206c39c 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -234,9 +234,7 @@ GRAMMAR EXTEND Gram
;
occs_nums:
[ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
- | "-"; n = nat_or_var; nl = LIST0 int_or_var ->
- (* have used int_or_var instead of nat_or_var for compatibility *)
- { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ]
+ | "-"; nl = LIST1 nat_or_var -> { AllOccurrencesBut nl } ] ]
;
occs:
[ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
@@ -379,9 +377,11 @@ GRAMMAR EXTEND Gram
{ {onhyps=None; concl_occs=occs} }
| "*"; "|-"; occs=concl_occ ->
{ {onhyps=None; concl_occs=occs} }
- | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ ->
+ | "|-"; occs=concl_occ ->
+ { {onhyps=Some []; concl_occs=occs} }
+ | hl = LIST1 hypident_occ SEP ","; "|-"; occs=concl_occ ->
{ {onhyps=Some hl; concl_occs=occs} }
- | hl=LIST0 hypident_occ SEP"," ->
+ | hl = LIST1 hypident_occ SEP "," ->
{ {onhyps=Some hl; concl_occs=NoOccurrences} } ] ]
;
clause_dft_concl:
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 26e2b18a02..77162ce89a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -13,7 +13,6 @@ open CErrors
open Util
open Names
open Nameops
-open Namegen
open Constr
open Context
open EConstr
@@ -485,7 +484,7 @@ let rec decompose_app_rel env evd t =
let (f', argl, argr) = decompose_app_rel env evd arg in
let ty = Retyping.get_type_of env evd argl in
let r = Retyping.relevance_of_type env evd ty in
- let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty,
+ let f'' = mkLambda (make_annot (Name Namegen.default_dependent_ident) r, ty,
mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty,
mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
in (f'', argl, argr)
@@ -1119,7 +1118,14 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
*)
| Lambda (n, t, b) when flags.under_lambdas ->
- let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
+ let unfresh, n' =
+ let id = match n.binder_name with
+ | Anonymous -> Namegen.default_dependent_ident
+ | Name id -> id
+ in
+ let id = Tactics.fresh_id_in_env unfresh id env in
+ Id.Set.add id unfresh, {n with binder_name = Name id}
+ in
let unfresh = match n'.binder_name with
| Anonymous -> unfresh
| Name id -> Id.Set.add id unfresh
@@ -1542,7 +1548,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
(* For compatibility *)
let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
let beta_hyp id = Tactics.reduct_in_hyp ~check:false ~reorder:false Reductionops.nf_betaiota (id, InHyp) in
- let treat sigma res =
+ let treat sigma res state =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
| Some None ->
@@ -1553,7 +1559,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let (undef, prf, newt) = res in
let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
let gls = List.rev (Evd.fold_undefined fold undef []) in
- let gls = List.map Proofview.with_empty_state gls in
+ let gls = List.map (fun gl -> Proofview.goal_with_state gl state) gls in
match clause, prf with
| Some id, Some p ->
let tac = tclTHENLIST [
@@ -1583,6 +1589,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
+ let state = Proofview.Goal.state gl in
let sigma = Tacmach.New.project gl in
let ty = match clause with
| None -> concl
@@ -1602,7 +1609,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause
in
let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
- treat sigma res <*>
+ treat sigma res state <*>
(* For compatibility *)
beta <*> Proofview.shelve_unifiable
with
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 3360a9a51c..21178a64a5 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -36,10 +36,8 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
module Table = Hashtbl.Make (Key)
exception InvalidTableFormat
- exception UnboundTable
- type mode = Closed | Open
- type 'a t = {outch : out_channel; mutable status : mode; htbl : 'a Table.t}
+ type 'a t = {outch : out_channel; htbl : 'a Table.t}
(* XXX: Move to Fun.protect once in Ocaml 4.08 *)
let fun_protect ~(finally : unit -> unit) work =
@@ -118,7 +116,6 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
close_in_noerr inch;
{ outch =
out_channel_of_descr (openfile f [O_WRONLY; O_APPEND; O_CREAT] 0o666)
- ; status = Open
; htbl }
with InvalidTableFormat ->
(* The file is corrupted *)
@@ -131,24 +128,20 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
(fun k e -> Marshal.to_channel outch (k, e) [Marshal.No_sharing])
htbl;
flush outch);
- {outch; status = Open; htbl}
+ {outch; htbl}
let add t k e =
- let {outch; status; htbl = tbl} = t in
- if status == Closed then raise UnboundTable
- else
- let fd = descr_of_out_channel outch in
- Table.add tbl k e;
- do_under_lock Write fd (fun _ ->
- Marshal.to_channel outch (k, e) [Marshal.No_sharing];
- flush outch)
+ let {outch; htbl = tbl} = t in
+ let fd = descr_of_out_channel outch in
+ Table.add tbl k e;
+ do_under_lock Write fd (fun _ ->
+ Marshal.to_channel outch (k, e) [Marshal.No_sharing];
+ flush outch)
let find t k =
- let {outch; status; htbl = tbl} = t in
- if status == Closed then raise UnboundTable
- else
- let res = Table.find tbl k in
- res
+ let {outch; htbl = tbl} = t in
+ let res = Table.find tbl k in
+ res
let memo cache f =
let tbl = lazy (try Some (open_in cache) with _ -> None) in
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index bd514f15d5..a4aa08300d 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -454,7 +454,7 @@ let ungen_upat lhs (sigma, uc, t) u =
let nb_cs_proj_args pc f u =
let na k =
- List.length (snd (lookup_canonical_conversion (GlobRef.ConstRef pc, k))).o_TCOMPS in
+ List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in
let nargs_of_proj t = match kind t with
| App(_,args) -> Array.length args
| Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 02:41:51 +0000