aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/common.ml7
-rw-r--r--plugins/extraction/common.mli1
-rw-r--r--plugins/extraction/ocaml.ml18
-rw-r--r--plugins/ltac/tacinterp.ml22
4 files changed, 29 insertions, 19 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 4a41f4c890..d215a7673d 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -604,6 +604,13 @@ let pp_global k r =
| Haskell -> if modular () then pp_haskell_gen k mp rls else s
| Ocaml -> pp_ocaml_gen k mp rls (Some l)
+(* Main name printing function for declaring a reference *)
+
+let pp_global_name k r =
+ let ls = ref_renaming (k,r) in
+ assert (List.length ls > 1);
+ List.hd ls
+
(* The next function is used only in Ocaml extraction...*)
let pp_module mp =
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 0bd9efd255..a482cfc03d 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -55,6 +55,7 @@ val opened_libraries : unit -> ModPath.t list
type kind = Term | Type | Cons | Mod
val pp_global : kind -> GlobRef.t -> string
+val pp_global_name : kind -> GlobRef.t -> string
val pp_module : ModPath.t -> string
val top_visible_mp : unit -> ModPath.t
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 088405da5d..6425c3111e 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -99,6 +99,8 @@ let str_global k r =
let pp_global k r = str (str_global k r)
+let pp_global_name k r = str (Common.pp_global k r)
+
let pp_modname mp = str (Common.pp_module mp)
(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *)
@@ -451,7 +453,7 @@ let pp_val e typ =
let pp_Dfix (rv,c,t) =
let names = Array.map
- (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
+ (fun r -> if is_inline_custom r then mt () else pp_global_name Term r) rv
in
let rec pp init i =
if i >= Array.length rv then mt ()
@@ -504,7 +506,7 @@ let pp_logical_ind packet =
fnl ()
let pp_singleton kn packet =
- let name = pp_global Type (GlobRef.IndRef (kn,0)) in
+ let name = pp_global_name Type (GlobRef.IndRef (kn,0)) in
let l = rename_tvars keywords packet.ip_vars in
hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
@@ -513,7 +515,7 @@ let pp_singleton kn packet =
let pp_record kn fields ip_equiv packet =
let ind = GlobRef.IndRef (kn,0) in
- let name = pp_global Type ind in
+ let name = pp_global_name Type ind in
let fieldnames = pp_fields ind fields in
let l = List.combine fieldnames packet.ip_types.(0) in
let pl = rename_tvars keywords packet.ip_vars in
@@ -535,7 +537,7 @@ let pp_ind co kn ind =
let nextkwd = fnl () ++ str "and " in
let names =
Array.mapi (fun i p -> if p.ip_logical then mt () else
- pp_global Type (GlobRef.IndRef (kn,i)))
+ pp_global_name Type (GlobRef.IndRef (kn,i)))
ind.ind_packets
in
let cnames =
@@ -575,7 +577,7 @@ let pp_decl = function
| Dterm (r,_,_) when is_inline_custom r -> mt ()
| Dind (kn,i) -> pp_mind kn i
| Dtype (r, l, t) ->
- let name = pp_global Type r in
+ let name = pp_global_name Type r in
let l = rename_tvars keywords l in
let ids, def =
try
@@ -592,7 +594,7 @@ let pp_decl = function
if is_custom r then str (" = " ^ find_custom r)
else pp_function (empty_env ()) a
in
- let name = pp_global Term r in
+ let name = pp_global_name Term r in
pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ())
| Dfix (rv,defs,typs) ->
pp_Dfix (rv,defs,typs)
@@ -603,10 +605,10 @@ let pp_spec = function
| Sind (kn,i) -> pp_mind kn i
| Sval (r,t) ->
let def = pp_type false [] t in
- let name = pp_global Term r in
+ let name = pp_global_name Term r in
hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
| Stype (r,vl,ot) ->
- let name = pp_global Type r in
+ let name = pp_global_name Type r in
let l = rename_tvars keywords vl in
let ids, def =
try
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 3228c6afd4..2ca9a0e69d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -182,7 +182,7 @@ let catch_error_with_trace_loc loc use_finer call_trace f x =
catching_error call_trace Exninfo.iraise e
let catch_error_loc loc use_finer tac =
- Proofview.tclOR tac (fun exn ->
+ Proofview.tclORELSE tac (fun exn ->
let (e, info) = update_loc loc use_finer exn in
Proofview.tclZERO ~info e)
@@ -1084,7 +1084,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
| _ -> value_interp ist >>= fun v -> return (name_vfun appl v)
-and eval_tactic ist tac : unit Proofview.tactic = match tac with
+and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
| TacAtom {loc;v=t} ->
let call = LtacAtomCall t in
let trace = push_trace(loc,call) ist in
@@ -1163,7 +1163,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l)
| TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
- | TacArg a -> interp_tactic ist (TacArg a)
+ | TacArg a -> Ftactic.run (val_interp ist tac) (fun v -> catch_error_loc a.CAst.loc false (tactic_of_value ist v))
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
@@ -1243,7 +1243,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
let ist = { lfun = Id.Map.empty; poly; extra } in
let appl = GlbAppl[r,[]] in
Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
- (val_interp ~appl ist (Tacenv.interp_ltac r))
+ (catch_error_tac_loc loc false trace (val_interp ~appl ist (Tacenv.interp_ltac r)))
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
@@ -1359,7 +1359,7 @@ and tactic_of_value ist vle =
lfun = lfun;
poly;
extra = TacStore.set ist.extra f_trace []; } in
- let tac = name_if_glob appl (eval_tactic ist t) in
+ let tac = name_if_glob appl (eval_tactic_ist ist t) in
Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
| VFun (appl,_,vmap,vars,_) ->
let tactic_nm =
@@ -1446,7 +1446,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
; poly
; extra = TacStore.set ist.extra f_trace trace
} in
- let tac = eval_tactic ist t in
+ let tac = eval_tactic_ist ist t in
let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in
catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy))
| _ -> Ftactic.return v
@@ -1927,11 +1927,11 @@ let default_ist () =
let eval_tactic t =
Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *)
Proofview.tclLIFT db_initialize <*>
- interp_tactic (default_ist ()) t
+ eval_tactic_ist (default_ist ()) t
let eval_tactic_ist ist t =
Proofview.tclLIFT db_initialize <*>
- interp_tactic ist t
+ eval_tactic_ist ist t
(** FFI *)
@@ -1977,7 +1977,7 @@ let interp_tac_gen lfun avoid_ids debug t =
let extra = TacStore.set extra f_avoid_ids avoid_ids in
let ist = { lfun; poly; extra } in
let ltacvars = Id.Map.domain lfun in
- interp_tactic ist
+ eval_tactic_ist ist
(intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
end
@@ -2094,7 +2094,7 @@ let () =
register_interp0 wit_tactic interp
let () =
- let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in
+ let interp ist tac = eval_tactic_ist ist tac >>= fun () -> Ftactic.return () in
register_interp0 wit_ltac interp
let () =
@@ -2121,7 +2121,7 @@ let _ =
let eval lfun poly env sigma ty tac =
let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
let ist = { lfun; poly; extra; } in
- let tac = interp_tactic ist tac in
+ let tac = eval_tactic_ist ist tac in
(* EJGA: We should also pass the proof name if desired, for now
poly seems like enough to get reasonable behavior in practice
*)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:35:07 +0000