aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--kernel/nativecode.mli2
-rw-r--r--kernel/nativelibrary.ml17
-rw-r--r--kernel/nativelibrary.mli2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--tactics/cbn.ml86
-rw-r--r--test-suite/bugs/closed/bug_13960.v10
-rw-r--r--user-contrib/Ltac2/tac2entries.ml13
8 files changed, 67 insertions, 67 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index d517d215ed..9ce388929c 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2130,7 +2130,7 @@ let compile_deps env sigma prefix init t =
in
aux env 0 init t
-let compile_constant_field env _prefix con acc cb =
+let compile_constant_field env con acc cb =
let gl = compile_constant env empty_evars con cb in
gl@acc
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 90525a19b2..17312ec8ea 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -65,7 +65,7 @@ val register_native_file : string -> unit
val is_loaded_native_file : string -> bool
-val compile_constant_field : env -> string -> Constant.t ->
+val compile_constant_field : env -> Constant.t ->
global list -> 'a constant_body -> global list
val compile_mind_field : ModPath.t -> Label.t ->
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 2e27fe071e..6dd7f315e0 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -17,21 +17,21 @@ open Nativecode
(** This file implements separate compilation for libraries in the native
compiler *)
-let rec translate_mod prefix mp env mod_expr acc =
+let rec translate_mod mp env mod_expr acc =
match mod_expr with
| NoFunctor struc ->
let env' = add_structure mp struc empty_delta_resolver env in
- List.fold_left (translate_field prefix mp env') acc struc
+ List.fold_left (translate_field mp env') acc struc
| MoreFunctor _ -> acc
-and translate_field prefix mp env acc (l,x) =
+and translate_field mp env acc (l,x) =
match x with
| SFBconst cb ->
let con = Constant.make2 mp l in
(debug_native_compiler (fun () ->
let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
Pp.str msg));
- compile_constant_field env prefix con acc cb
+ compile_constant_field env con acc cb
| SFBmind mb ->
(debug_native_compiler (fun () ->
let id = mb.mind_packets.(0).mind_typename in
@@ -45,7 +45,7 @@ and translate_field prefix mp env acc (l,x) =
Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
in
Pp.str msg));
- translate_mod prefix mp env md.mod_type acc
+ translate_mod mp env md.mod_type acc
| SFBmodtype mdtyp ->
let mp = mdtyp.mod_mp in
(debug_native_compiler (fun () ->
@@ -53,19 +53,18 @@ and translate_field prefix mp env acc (l,x) =
Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
in
Pp.str msg));
- translate_mod prefix mp env mdtyp.mod_type acc
+ translate_mod mp env mdtyp.mod_type acc
-let dump_library mp dp env mod_expr =
+let dump_library mp env mod_expr =
debug_native_compiler (fun () -> Pp.str "Compiling library...");
match mod_expr with
| NoFunctor struc ->
let env = add_structure mp struc empty_delta_resolver env in
- let prefix = mod_uid_of_dirpath dp ^ "." in
let t0 = Sys.time () in
clear_global_tbl ();
clear_symbols ();
let mlcode =
- List.fold_left (translate_field prefix mp env) [] struc
+ List.fold_left (translate_field mp env) [] struc
in
let t1 = Sys.time () in
let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index 8f58dfa8d3..1d0d56703d 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -15,5 +15,5 @@ open Nativecode
(** This file implements separate compilation for libraries in the native
compiler *)
-val dump_library : ModPath.t -> DirPath.t -> env -> module_signature ->
+val dump_library : ModPath.t -> env -> module_signature ->
global list * Nativevalues.symbols
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a35f94e3ce..5f83e78eb0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1273,7 +1273,7 @@ let export ?except ~output_native_objects senv dir =
in
let ast, symbols =
if output_native_objects then
- Nativelibrary.dump_library mp dir senv.env str
+ Nativelibrary.dump_library mp senv.env str
else [], Nativevalues.empty_symbols
in
let lib = {
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 167f7d4026..99d579f5c6 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -402,11 +402,11 @@ let safe_meta_value sigma ev =
(* Beta Reduction tools *)
-let apply_subst recfun env sigma refold cst_l t stack =
+let apply_subst recfun env sigma cst_l t stack =
let rec aux env cst_l t stack =
match (Stack.decomp stack, EConstr.kind sigma t) with
| Some (h,stacktl), Lambda (_,_,c) ->
- let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in
+ let cst_l' = Cst_stack.add_param h cst_l in
aux (h::env) cst_l' c stacktl
| _ -> recfun sigma cst_l (substl env t, stack)
in aux env cst_l t stack
@@ -453,50 +453,42 @@ let magically_constant_of_fixbody env sigma reference bd = function
| None -> bd
end
-let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
+let contract_cofix ~env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
let nbodies = Array.length bodies in
let make_Fi j =
let ind = nbodies-j-1 in
if Int.equal bodynum ind then mkCoFix (ind,typedbodies)
else
let bd = mkCoFix (ind,typedbodies) in
- match env with
+ match reference with
| None -> bd
- | Some e ->
- match reference with
- | None -> bd
- | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+ | Some r -> magically_constant_of_fixbody env sigma r bd names.(ind).binder_name in
let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
(** Similar to the "fix" case below *)
-let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
+let reduce_and_refold_cofix recfun env sigma cst_l cofix sk =
let raw_answer =
- let env = if refold then Some env else None in
- contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
+ contract_cofix ~env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
apply_subst
(fun sigma x (t,sk') ->
- let t' =
- if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in
+ let t' = Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t in
recfun x (t',sk'))
- [] sigma refold Cst_stack.empty raw_answer sk
+ [] sigma Cst_stack.empty raw_answer sk
(* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
-let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
+let contract_fix ~env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
let nbodies = Array.length recindices in
let make_Fi j =
let ind = nbodies-j-1 in
if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies)
else
let bd = mkFix ((recindices,ind),typedbodies) in
- match env with
+ match reference with
| None -> bd
- | Some e ->
- match reference with
- | None -> bd
- | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+ | Some r -> magically_constant_of_fixbody env sigma r bd names.(ind).binder_name in
let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
@@ -504,18 +496,14 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies
replace the fixpoint by the best constant from [cst_l]
Other rels are directly substituted by constants "magically found from the
context" in contract_fix *)
-let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
+let reduce_and_refold_fix recfun env sigma cst_l fix sk =
let raw_answer =
- let env = if refold then Some env else None in
- contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
+ contract_fix ~env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
apply_subst
(fun sigma x (t,sk') ->
- let t' =
- if refold then
- Cst_stack.best_replace sigma (mkFix fix) cst_l t
- else t
- in recfun x (t',sk'))
- [] sigma refold Cst_stack.empty raw_answer sk
+ let t' = Cst_stack.best_replace sigma (mkFix fix) cst_l t in
+ recfun x (t',sk'))
+ [] sigma Cst_stack.empty raw_answer sk
module CredNative = Reductionops.CredNative
@@ -524,7 +512,7 @@ module CredNative = Reductionops.CredNative
Here is where unfolded constant are stored in order to be
eventually refolded.
- If tactic_mode is true, it uses ReductionBehaviour, prefers
+ It uses ReductionBehaviour, prefers
refold constant instead of value and tries to infer constants
fix and cofix came from.
@@ -558,7 +546,7 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
in
Vars.substl subst (snd br)
-let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
+let rec whd_state_gen ?csts flags env sigma =
let open Context.Named.Declaration in
let open ReductionBehaviour in
let rec whrec cst_l (x, stack) =
@@ -584,7 +572,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
(match lookup_named id env with
| LocalDef (_,body,_) ->
- whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack)
+ whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack)
| _ -> fold ())
| Evar ev -> fold ()
| Meta ev ->
@@ -600,10 +588,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| body ->
begin
let body = EConstr.of_constr body in
- if not tactic_mode
- then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
- (body, stack)
- else (* Looks for ReductionBehaviour *)
+ (* Looks for ReductionBehaviour *)
match ReductionBehaviour.get (GlobRef.ConstRef c) with
| None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
| Some behavior ->
@@ -652,10 +637,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
else fold ()
| Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
(let npars = Projection.npars p in
- if not tactic_mode then
- let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in
- whrec Cst_stack.empty stack'
- else match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with
+ match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with
| None ->
let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
let stack'', csts = whrec Cst_stack.empty stack' in
@@ -693,24 +675,24 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
end)
| LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
- apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack
+ apply_subst (fun _ -> whrec) [b] sigma cst_l c stack
| Cast (c,_,_) -> whrec cst_l (c, stack)
| App (f,cl) ->
whrec
- (if refold then Cst_stack.add_args cl cst_l else cst_l)
+ (Cst_stack.add_args cl cst_l)
(f, Stack.append_app cl stack)
| Lambda (na,t,c) ->
(match Stack.decomp stack with
| Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
- apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack
+ apply_subst (fun _ -> whrec) [] sigma cst_l x stack
| None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
let env' = push_rel (LocalAssum (na, t)) env in
- let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in
- (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with
+ let whrec' = whd_state_gen flags env' sigma in
+ (match EConstr.kind sigma (Stack.zip ~refold:true sigma (whrec' (c, Stack.empty))) with
| App (f,cl) ->
let napp = Array.length cl in
if napp > 0 then
- let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in
+ let (x', l') = whrec' (Array.last cl, Stack.empty) in
match EConstr.kind sigma x', l' with
| Rel 1, [] ->
let lc = Array.sub cl 0 (napp-1) in
@@ -743,7 +725,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
let x' = Stack.zip sigma (x, args) in
let out_sk = s' @ (Stack.append_app [|x'|] s'') in
- reduce_and_refold_fix whrec env sigma refold cst_l f out_sk
+ reduce_and_refold_fix whrec env sigma cst_l f out_sk
|args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') ->
let x' = Stack.zip sigma (x, args) in
begin match remains with
@@ -755,7 +737,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| Some body ->
let const = (fst const, EInstance.make (snd const)) in
let body = EConstr.of_constr body in
- whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
+ whrec (Cst_stack.add_cst (mkConstU const) cst_l)
(body, s' @ (Stack.append_app [|x'|] s'')))
| Stack.Cst_proj p ->
let stack = s' @ (Stack.append_app [|x'|] s'') in
@@ -778,7 +760,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
match Stack.strip_app stack with
|args, ((Stack.Case _ |Stack.Proj _)::s') ->
- reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack
+ reduce_and_refold_cofix whrec env sigma cst_l cofix stack
|_ -> fold ()
else fold ()
@@ -812,12 +794,10 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
in
fun xs ->
let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
- if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res
+ (Stack.best_state sigma s cst_l)
let whd_cbn flags env sigma t =
- let (state,_) =
- (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty))
- in
+ let state = whd_state_gen flags env sigma (t, Stack.empty) in
Stack.zip ~refold:true sigma state
let norm_cbn flags env sigma t =
diff --git a/test-suite/bugs/closed/bug_13960.v b/test-suite/bugs/closed/bug_13960.v
new file mode 100644
index 0000000000..947db9586f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13960.v
@@ -0,0 +1,10 @@
+Require Ltac2.Ltac2.
+
+Set Default Goal Selector "!".
+
+Ltac2 t () := let _ := Message.print (Message.of_string "hi") in 42.
+
+Goal False.
+Proof.
+Ltac2 Eval t ().
+Abort.
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index d0655890a7..faa1e74728 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -816,7 +816,18 @@ let perform_eval ~pstate e =
| Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v
| Goal_select.SelectId id -> Proofview.tclFOCUSID id v
| Goal_select.SelectAll -> v
- | Goal_select.SelectAlreadyFocused -> assert false (* TODO **)
+ | Goal_select.SelectAlreadyFocused ->
+ let open Proofview.Notations in
+ Proofview.numgoals >>= fun n ->
+ if Int.equal n 1 then v
+ else
+ let e = CErrors.UserError
+ (None,
+ Pp.(str "Expected a single focused goal but " ++
+ int n ++ str " goals are focused."))
+ in
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info e
in
let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in
let { Proof.sigma } = Proof.data proof in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 02:05:23 +0000