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/funind/functional_principles_proofs.ml16
-rw-r--r--plugins/funind/gen_principle.ml10
-rw-r--r--plugins/funind/recdef.ml25
-rw-r--r--plugins/ltac/g_obligations.mlg22
-rw-r--r--plugins/ltac/tacinterp.ml70
-rw-r--r--plugins/micromega/certificate.ml5
-rw-r--r--plugins/micromega/zify.ml11
-rw-r--r--plugins/omega/coq_omega.ml192
-rw-r--r--plugins/ssr/ssrast.mli8
-rw-r--r--plugins/ssr/ssrcommon.ml12
-rw-r--r--plugins/ssr/ssrelim.ml28
-rw-r--r--plugins/ssr/ssrequality.ml2
-rw-r--r--plugins/ssr/ssrview.ml10
16 files changed, 259 insertions, 178 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/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 14d0c04212..72e6006b7e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -483,7 +483,10 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos g =
(Proofview.V82.of_tactic
(intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps)))
; (* Then the equation itself *)
- Proofview.V82.of_tactic (intro_using heq_id)
+ Proofview.V82.of_tactic
+ (intro_using_then heq_id
+ (* we get the fresh name with onLastHypId *)
+ (fun _ -> Proofview.tclUNIT ()))
; onLastHypId (fun heq_id ->
tclTHENLIST
[ (* Then the new hypothesis *)
@@ -864,7 +867,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
in
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
+ ~idopt:None
in
evd
@@ -1112,16 +1116,18 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num
in
let first_tac : tactic =
(* every operations until fix creations *)
+ (* names are already refreshed *)
tclTHENLIST
[ observe_tac "introducing params"
(Proofview.V82.of_tactic
- (intros_using (List.rev_map id_of_decl princ_info.params)))
+ (intros_mustbe_force (List.rev_map id_of_decl princ_info.params)))
; observe_tac "introducing predictes"
(Proofview.V82.of_tactic
- (intros_using (List.rev_map id_of_decl princ_info.predicates)))
+ (intros_mustbe_force
+ (List.rev_map id_of_decl princ_info.predicates)))
; observe_tac "introducing branches"
(Proofview.V82.of_tactic
- (intros_using (List.rev_map id_of_decl princ_info.branches)))
+ (intros_mustbe_force (List.rev_map id_of_decl princ_info.branches)))
; observe_tac "building fixes" mk_fixes ]
in
let intros_after_fixes : tactic =
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index ffce2f8c85..45b1713441 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1526,9 +1526,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
let lemma =
fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
in
- let (_ : GlobRef.t list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
- ~idopt:None
+ let (_ : _ list) =
+ Declare.Proof.save_regular ~proof:lemma
+ ~opaque:Vernacexpr.Transparent ~idopt:None
in
let finfo =
match find_Function_infos (fst f_as_constant) with
@@ -1599,8 +1599,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
lemma)
in
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
- ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma
+ ~opaque:Vernacexpr.Transparent ~idopt:None
in
let finfo =
match find_Function_infos (fst f_as_constant) with
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 64f62ba1fb..066ade07d2 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -59,7 +59,8 @@ let declare_fun name kind ?univs value =
let defined lemma =
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
+ ~idopt:None
in
()
@@ -413,7 +414,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
observe_tclTHENLIST
(fun _ _ -> str "treat_case1")
[ h_intros (List.rev rev_ids)
- ; Proofview.V82.of_tactic (intro_using teq_id)
+ ; Proofview.V82.of_tactic
+ (intro_using_then teq_id (fun _ -> Proofview.tclUNIT ()))
; onLastHypId (fun heq ->
observe_tclTHENLIST
(fun _ _ -> str "treat_case2")
@@ -600,7 +602,11 @@ let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds g =
(Proofview.V82.of_tactic (simplest_case (mkVar id)))
[ observe_tclTHENLIST
(fun _ _ -> str "")
- [ Proofview.V82.of_tactic (intro_using h_id)
+ [ Proofview.V82.of_tactic
+ (intro_using_then h_id
+ (* We don't care about the refreshed name,
+ accessed only through auto? *)
+ (fun _ -> Proofview.tclUNIT ()))
; Proofview.V82.of_tactic
(simplest_elim
(mkApp (delayed_force lt_n_O, [|s_max|])))
@@ -864,7 +870,10 @@ let terminate_app_rec (f, args) expr_info continuation_tac _ g =
(simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args))))
[ observe_tclTHENLIST
(fun _ _ -> str "terminate_app_rec2")
- [ Proofview.V82.of_tactic (intro_using rec_res_id)
+ [ Proofview.V82.of_tactic
+ (intro_using_then rec_res_id
+ (* refreshed name gotten from onNthHypId *)
+ (fun _ -> Proofview.tclUNIT ()))
; Proofview.V82.of_tactic intro
; onNthHypId 1 (fun v_bound ->
onNthHypId 2 (fun v ->
@@ -1503,7 +1512,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
in
let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
let (_ : _ list) =
- Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
+ Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None
in
()
in
@@ -1662,7 +1671,11 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
in
let _ =
Flags.silently
- (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None)
+ (fun () ->
+ let (_ : _ list) =
+ Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None
+ in
+ ())
()
in
()
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 81ee6ed5bb..fa176482bf 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,14 +80,14 @@ GRAMMAR EXTEND Gram
open Declare.Obls
-let obligation obl tac = with_tac (fun t -> obligation obl t) tac
-let next_obligation obl tac = with_tac (fun t -> next_obligation obl t) tac
+let obligation ~pm obl tac = with_tac (fun t -> obligation ~pm obl t) tac
+let next_obligation ~pm obl tac = with_tac (fun t -> next_obligation ~pm obl t) tac
let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
}
-VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof
+VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program
| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, Some name, Some t) tac }
| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
@@ -101,14 +101,14 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_pro
| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
END
-VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
{ try_solve_obligation num None (Some (Tacinterp.interp t)) }
END
-VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligations" "with" tactic(t) ] ->
@@ -117,14 +117,14 @@ VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF
{ try_solve_obligations None None }
END
-VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "All" "Obligations" "with" tactic(t) ] ->
{ solve_all_obligations (Some (Tacinterp.interp t)) }
| [ "Solve" "All" "Obligations" ] ->
{ solve_all_obligations None }
END
-VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Admit" "Obligations" "of" ident(name) ] -> { admit_obligations (Some name) }
| [ "Admit" "Obligations" ] -> { admit_obligations None }
END
@@ -148,14 +148,14 @@ VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) }
END
-VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program
| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) }
| [ "Obligations" ] -> { show_obligations None }
END
-VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_notice (show_term (Some name)) }
-| [ "Preterm" ] -> { Feedback.msg_notice (show_term None) }
+VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program
+| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) }
+| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) }
END
{
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fdebe14a23..2ca9a0e69d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -161,27 +161,45 @@ let catching_error call_trace fail (e, info) =
fail located_exc
end
-let update_loc ?loc (e, info) =
- (e, Option.cata (Loc.add_loc info) info loc)
+let update_loc loc use_finer (e, info as e') =
+ match loc with
+ | Some loc ->
+ if use_finer then
+ (* ensure loc if there is none *)
+ match Loc.get_loc info with
+ | None -> (e, Loc.add_loc info loc)
+ | _ -> (e, info)
+ else
+ (* override loc (because loc refers to inside of Ltac functions) *)
+ (e, Loc.add_loc info loc)
+ | None -> e'
-let catch_error ?loc call_trace f x =
+let catch_error_with_trace_loc loc use_finer call_trace f x =
try f x
with e when CErrors.noncritical e ->
let e = Exninfo.capture e in
- let e = update_loc ?loc e in
+ let e = update_loc loc use_finer e in
catching_error call_trace Exninfo.iraise e
-let catch_error_loc ?loc tac =
- Proofview.tclOR tac (fun exn ->
- let (e, info) = update_loc ?loc exn in
+let catch_error_loc loc use_finer tac =
+ Proofview.tclORELSE tac (fun exn ->
+ let (e, info) = update_loc loc use_finer exn in
Proofview.tclZERO ~info e)
-let wrap_error ?loc tac k =
+let wrap_error tac k =
+ if is_traced () then Proofview.tclORELSE tac k else tac
+
+let wrap_error_loc loc use_finer tac k =
if is_traced () then Proofview.tclORELSE tac k
- else catch_error_loc ?loc tac
+ else catch_error_loc loc use_finer tac
+
+let catch_error_tac call_trace tac =
+ wrap_error
+ tac
+ (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
-let catch_error_tac ?loc call_trace tac =
- wrap_error ?loc
+let catch_error_tac_loc loc use_finer call_trace tac =
+ wrap_error_loc loc use_finer
tac
(catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
@@ -553,7 +571,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
let loc = loc_of_glob_constr term in
let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in
let (evd,c) =
- catch_error ?loc trace (understand_ltac flags env sigma vars kind) term
+ catch_error_with_trace_loc loc true trace (understand_ltac flags env sigma vars kind) term
in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
@@ -1066,12 +1084,12 @@ 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
Profile_ltac.do_profile "eval_tactic:2" trace
- (catch_error_tac ?loc trace (interp_atomic ist t))
+ (catch_error_tac_loc loc true trace (interp_atomic ist t))
| TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
| TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
| TacId s ->
@@ -1145,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)} ->
@@ -1162,7 +1180,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
; poly
; extra = TacStore.set ist.extra f_trace trace } in
val_interp ist alias.Tacenv.alias_body >>= fun v ->
- Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v))
+ Ftactic.lift (catch_error_loc loc false (tactic_of_value ist v))
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
@@ -1191,7 +1209,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
let tac args =
let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
- Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist))
+ Proofview.Trace.name_tactic name (catch_error_tac_loc loc false trace (tac args ist))
in
Ftactic.run args tac
@@ -1225,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
@@ -1294,7 +1312,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
; extra = TacStore.set ist.extra f_trace []
} in
Profile_ltac.do_profile "interp_app" trace ~count_call:false
- (catch_error_tac ?loc trace (val_interp ist body)) >>= fun v ->
+ (catch_error_tac_loc loc false trace (val_interp ist body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
@@ -1341,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 =
@@ -1428,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
@@ -1909,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 *)
@@ -1959,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
@@ -2076,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 () =
@@ -2103,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
*)
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 9eeba614c7..148c1772bf 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -1020,10 +1020,11 @@ let lia (can_enum : bool) (prfdepth : int) sys =
p)
sys
end;
+ let bnd1 = bound_monomials sys in
let sys = subst sys in
- let bnd = bound_monomials sys in
+ let bnd2 = bound_monomials sys in
(* To deal with non-linear monomials *)
- let sys = bnd @ saturate_by_linear_equalities sys @ sys in
+ let sys = bnd1 @ bnd2 @ saturate_by_linear_equalities sys @ sys in
let sys' = List.map (fun ((p, o), prf) -> (cstr_of_poly (p, o), prf)) sys in
xlia (List.map fst sys) can_enum reduction_equations sys'
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 4e1f9a66ac..fa29e6080e 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -1324,9 +1324,14 @@ let do_let tac (h : Constr.named_declaration) =
let env = Tacmach.New.pf_env gl in
let evd = Tacmach.New.project gl in
try
- ignore (get_injection env evd (EConstr.of_constr ty));
- tac id.Context.binder_name (EConstr.of_constr t)
- (EConstr.of_constr ty)
+ let x = id.Context.binder_name in
+ ignore
+ (let eq = Lazy.force eq in
+ find_option
+ (match_operator env evd eq
+ [|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|])
+ (HConstr.find_all eq !table_cache));
+ tac x (EConstr.of_constr t) (EConstr.of_constr ty)
with Not_found -> Tacticals.New.tclIDTAC)
let iter_let_aux tac =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 3ba6365783..cd5b747d75 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1055,6 +1055,9 @@ let rec clear_zero p = function
let tac,t = clear_zero (P_APP 2 :: p) r in tac,Oplus(f,t)
| t -> [],t
+open Proofview
+open Proofview.Notations
+
let replay_history tactic_normalisation =
let aux = Id.of_string "auxiliary" in
let aux1 = Id.of_string "auxiliary_1" in
@@ -1085,8 +1088,8 @@ let replay_history tactic_normalisation =
mk_integer k;
mkVar id1; mkVar id2 |])];
mk_then tac;
- (intros_using [aux]);
- resolve_id aux;
+ intro_using_then aux (fun aux ->
+ resolve_id aux);
reflexivity
]
| CONTRADICTION (e1,e2) :: l ->
@@ -1128,24 +1131,25 @@ let replay_history tactic_normalisation =
tclTHENS
(cut state_eg)
[ tclTHENS
- (tclTHENLIST [
- (intros_using [aux]);
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA1,
- [| eq1; rhs; mkVar aux; mkVar id |])]);
- (clear [aux;id]);
- (intros_using [id]);
- (cut (mk_gt kk dd)) ])
+ (intro_using_then aux (fun aux ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA1,
+ [| eq1; rhs; mkVar aux; mkVar id |])]);
+ (clear [aux;id]);
+ (intro_mustbe_force id);
+ (cut (mk_gt kk dd)) ]))
[ tclTHENS
(cut (mk_gt kk izero))
- [ tclTHENLIST [
- (intros_using [aux1; aux2]);
+ [ intro_using_then aux1 (fun aux1 ->
+ intro_using_then aux2 (fun aux2 ->
+ tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_Zmult_le_approx,
[| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]);
(clear [aux1;aux2;id]);
- (intros_using [id]);
- (loop l) ];
+ (intro_mustbe_force id);
+ (loop l) ]));
tclTHENLIST [
(unfold sp_Zgt);
simpl_in_concl;
@@ -1166,21 +1170,24 @@ let replay_history tactic_normalisation =
tclTHENS
(cut (mk_gt dd izero))
[ tclTHENS (cut (mk_gt kk dd))
- [tclTHENLIST [
- (intros_using [aux2;aux1]);
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA4,
- [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
- (clear [aux1;aux2]);
- unfold sp_not;
- (intros_using [aux]);
- resolve_id aux;
- mk_then tac;
- assumption ] ;
- tclTHENLIST [
- unfold sp_Zgt;
- simpl_in_concl;
- reflexivity ] ];
+ [ intro_using_then aux2 (fun aux2 ->
+ intro_using_then aux1 (fun aux1 ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA4,
+ [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
+ (clear [aux1;aux2]);
+ unfold sp_not;
+ intro_using_then aux (fun aux ->
+ tclTHENLIST [
+ resolve_id aux;
+ mk_then tac;
+ assumption
+ ])])) ;
+ tclTHENLIST [
+ unfold sp_Zgt;
+ simpl_in_concl;
+ reflexivity ] ];
tclTHENLIST [
unfold sp_Zgt;
simpl_in_concl;
@@ -1196,29 +1203,30 @@ let replay_history tactic_normalisation =
let tac = scalar_norm [P_APP 3] e2.body in
tclTHENS
(cut state_eq)
- [tclTHENLIST [
- (intros_using [aux1]);
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA18,
- [| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
- (clear [aux1;id]);
- (intros_using [id]);
- (loop l) ];
- tclTHEN (mk_then tac) reflexivity ]
+ [ intro_using_then aux1 (fun aux1 ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA18,
+ [| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
+ (clear [aux1;id]);
+ (intro_mustbe_force id);
+ (loop l) ]);
+ tclTHEN (mk_then tac) reflexivity ]
else
let tac = scalar_norm [P_APP 3] e2.body in
tclTHENS (cut state_eq)
[
tclTHENS
(cut (mk_gt kk izero))
- [tclTHENLIST [
- (intros_using [aux2;aux1]);
- (generalize_tac
+ [ intro_using_then aux2 (fun aux2 ->
+ intro_using_then aux1 (fun aux1 ->
+ tclTHENLIST [
+ (generalize_tac
[mkApp (Lazy.force coq_OMEGA3,
[| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
(clear [aux1;aux2;id]);
- (intros_using [id]);
- (loop l) ];
+ (intro_mustbe_force id);
+ (loop l) ]));
tclTHENLIST [
unfold sp_Zgt;
simpl_in_concl;
@@ -1238,13 +1246,13 @@ let replay_history tactic_normalisation =
in
tclTHENS
(cut (mk_eq eq1 (mk_inv eq2)))
- [tclTHENLIST [
- (intros_using [aux]);
- (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
- [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
- (clear [id1;id2;aux]);
- (intros_using [id]);
- (loop l) ];
+ [ intro_using_then aux (fun aux ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
+ (clear [id1;id2;aux]);
+ (intro_mustbe_force id);
+ (loop l) ]);
tclTHEN (mk_then tac) reflexivity]
| STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l ->
@@ -1271,18 +1279,19 @@ let replay_history tactic_normalisation =
orig.body m ({c= negone;v= v}::def.body) in
tclTHENS
(cut theorem)
- [tclTHENLIST [
- (intros_using [aux]);
- (elim_id aux);
- (clear [aux]);
- (intros_using [vid; aux]);
- (generalize_tac
+ [ tclTHENLIST [ intro_using_then aux (fun aux ->
+ (elim_id aux) <*>
+ (clear [aux]));
+ intro_using_then vid (fun vid ->
+ intro_using_then aux (fun aux ->
+ tclTHENLIST [
+ (generalize_tac
[mkApp (Lazy.force coq_OMEGA9,
[| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
mk_then tac;
(clear [aux]);
- (intros_using [id]);
- (loop l) ];
+ (intro_mustbe_force id);
+ (loop l) ]))];
tclTHEN (exists_tac eq1) reflexivity ]
| SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
let id1 = new_identifier ()
@@ -1294,8 +1303,8 @@ let replay_history tactic_normalisation =
let eq = val_of(decompile e) in
tclTHENS
(simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))
- [tclTHENLIST [ mk_then tac1; (intros_using [id1]); (loop act1) ];
- tclTHENLIST [ mk_then tac2; (intros_using [id2]); (loop act2) ]]
+ [tclTHENLIST [ mk_then tac1; (intro_mustbe_force id1); (loop act1) ];
+ tclTHENLIST [ mk_then tac2; (intro_mustbe_force id2); (loop act2) ]]
| SUM(e3,(k1,e1),(k2,e2)) :: l ->
let id = new_identifier () in
tag_hypothesis id e3;
@@ -1318,7 +1327,7 @@ let replay_history tactic_normalisation =
(generalize_tac
[mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
mk_then tac;
- (intros_using [id]);
+ (intro_mustbe_force id);
(loop l)
]
else
@@ -1329,25 +1338,26 @@ let replay_history tactic_normalisation =
tclTHENS (cut (mk_gt kk1 izero))
[tclTHENS
(cut (mk_gt kk2 izero))
- [tclTHENLIST [
- (intros_using [aux2;aux1]);
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA7, [|
- eq1;eq2;kk1;kk2;
- mkVar aux1;mkVar aux2;
- mkVar id1;mkVar id2 |])]);
- (clear [aux1;aux2]);
- mk_then tac;
- (intros_using [id]);
- (loop l) ];
- tclTHENLIST [
- unfold sp_Zgt;
- simpl_in_concl;
- reflexivity ] ];
- tclTHENLIST [
- unfold sp_Zgt;
- simpl_in_concl;
- reflexivity ] ]
+ [ intro_using_then aux2 (fun aux2 ->
+ intro_using_then aux1 (fun aux1 ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_OMEGA7, [|
+ eq1;eq2;kk1;kk2;
+ mkVar aux1;mkVar aux2;
+ mkVar id1;mkVar id2 |])]);
+ (clear [aux1;aux2]);
+ mk_then tac;
+ (intro_mustbe_force id);
+ (loop l) ]));
+ tclTHENLIST [
+ unfold sp_Zgt;
+ simpl_in_concl;
+ reflexivity ] ];
+ tclTHENLIST [
+ unfold sp_Zgt;
+ simpl_in_concl;
+ reflexivity ] ]
| CONSTANT_NOT_NUL(e,k) :: l ->
tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
| CONSTANT_NUL(e) :: l ->
@@ -1358,9 +1368,8 @@ let replay_history tactic_normalisation =
unfold sp_Zle;
simpl_in_concl;
unfold sp_not;
- (intros_using [aux]);
- resolve_id aux;
- reflexivity
+ intro_using_then aux (fun aux ->
+ resolve_id aux <*> reflexivity)
]
| _ -> Proofview.tclUNIT ()
in
@@ -1382,7 +1391,7 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
in
if not (List.is_empty tac) then
let id' = new_identifier () in
- ((id',(tclTHENLIST [ shift_left; mk_then tac; (intros_using [id']) ]))
+ ((id',(tclTHENLIST [ shift_left; mk_then tac; (intro_mustbe_force id') ]))
:: tactic,
compile id' flag t' :: defs)
else
@@ -1423,10 +1432,7 @@ let destructure_omega env sigma tac_def (id,c) =
let reintroduce id =
(* [id] cannot be cleared if dependent: protect it by a try *)
- tclTHEN (tclTRY (clear [id])) (intro_using id)
-
-
-open Proofview.Notations
+ tclTHEN (tclTRY (clear [id])) (intro_using_then id (fun _ -> tclUNIT()))
let coq_omega =
Proofview.Goal.enter begin fun gl ->
@@ -1444,10 +1450,10 @@ let coq_omega =
tag_hypothesis id i;
(tclTHENLIST [
(simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
- (intros_using [v; id]);
+ (intros_mustbe_force [v; id]);
(elim_id id);
(clear [id]);
- (intros_using [th;id]);
+ (intros_mustbe_force [th;id]);
tac ]),
{kind = INEQ;
body = [{v=intern_id v; c=one}];
@@ -1455,7 +1461,7 @@ let coq_omega =
else
(tclTHENLIST [
(simplest_elim (applist (Lazy.force coq_new_var, [t])));
- (intros_using [v;th]);
+ (intros_mustbe_force [v;th]);
tac ]),
sys)
(Proofview.tclUNIT (),[]) (dump_tables ())
@@ -1508,7 +1514,7 @@ let nat_inject =
tclTHENS
(tclTHEN
(simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1])))
- (intros_using [id]))
+ (intro_mustbe_force id))
[
tclTHENLIST [
(clever_rewrite_gen p
@@ -1703,7 +1709,7 @@ let onClearedName2 id tac =
(tclTRY (clear [id]))
(Proofview.Goal.enter begin fun gl ->
let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in
- let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in
+ let id2 = fresh_id (Id.Set.singleton id1) (add_suffix id "_right") gl in
tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
end)
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 8adffdc709..f6a741f468 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -51,13 +51,19 @@ type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
(* NEW ssr term *)
+type ast_glob_env = {
+ ast_ltacvars : Id.Set.t;
+ ast_extra : Genintern.Store.t;
+ ast_intern_sign : Genintern.intern_variable_status;
+}
+
(* These terms are raw but closed with the intenalization/interpretation
* context. It is up to the tactic receiving it to decide if such contexts
* are useful or not, and eventually manipulate the term before turning it
* into a constr *)
type ast_closure_term = {
body : Constrexpr.constr_expr;
- glob_env : Genintern.glob_sign option; (* for Tacintern.intern_constr *)
+ glob_env : ast_glob_env option; (* for Tacintern.intern_constr *)
interp_env : Geninterp.interp_sign option; (* for Tacinterp.interp_open_constr_with_bindings *)
annotation : [ `None | `Parens | `DoubleParens | `At ];
}
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 65204b7868..d859fe51ab 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -302,6 +302,11 @@ let mk_ast_closure_term a t = {
}
let glob_ast_closure_term (ist : Genintern.glob_sign) t =
+ let ist = {
+ ast_ltacvars = ist.Genintern.ltacvars;
+ ast_intern_sign = ist.Genintern.intern_sign;
+ ast_extra = ist.Genintern.extra;
+ } in
{ t with glob_env = Some ist }
let subst_ast_closure_term (_s : Mod_subst.substitution) t =
(* _s makes sense only for glob constr *)
@@ -1042,7 +1047,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc =
let uct = Evd.evar_universe_context (fst oc) in
let n, oc = abs_evars_pirrel env sigma (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*>
- Proofview.tclOR (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc))
+ Proofview.tclORELSE (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc))
(fun _ -> Proofview.tclZERO dependent_apply_error)
end
@@ -1124,8 +1129,7 @@ let tclDO n tac =
let _, info = Exninfo.capture e in
let e' = CErrors.UserError (l, prefix i ++ s) in
Exninfo.iraise (e', info)
- | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) ->
- raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+ in
let rec loop i gl =
if i = n then tac_err_at i gl else
(tclTHEN (tac_err_at i) (loop (i + 1))) gl in
@@ -1348,7 +1352,7 @@ let unsafe_intro env decl b =
Refine.refine ~typecheck:false begin fun sigma ->
let ctx = Environ.named_context_val env in
let nctx = EConstr.push_named_context_val decl ctx in
- let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in
+ let inst = EConstr.identity_subst_val (Environ.named_context_val env) in
let ninst = EConstr.mkRel 1 :: inst in
let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index a12b4aad11..1e182b52fa 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -485,18 +485,22 @@ let revtoptac n0 =
Logic.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])))
end
-let equality_inj l b id c =
- Proofview.V82.tactic begin fun gl ->
- let msg = ref "" in
- try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
- with
- | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s))
- | CErrors.UserError (_,s)
- when msg := Pp.string_of_ppcmds s;
- !msg = "Not a projectable equality but a discriminable one." ||
- !msg = "Nothing to inject." ->
- Feedback.msg_warning (Pp.str !msg);
- discharge_hyp (id, (id, "")) gl
+let nothing_to_inject =
+ CWarnings.create ~name:"spurious-ssr-injection" ~category:"ssr"
+ (fun (sigma, env, ty) ->
+ Pp.(str "SSReflect: cannot obtain new equations out of" ++ fnl() ++
+ str" " ++ Printer.pr_econstr_env env sigma ty ++ fnl() ++
+ str "Did you write an extra [] in the intro pattern?"))
+
+let equality_inj l b id c = Proofview.Goal.enter begin fun gl ->
+ Proofview.tclORELSE (Equality.inj None l b None c)
+ (function
+ | (Equality.NothingToInject,_) ->
+ let open Proofview.Notations in
+ Ssrcommon.tacTYPEOF (EConstr.mkVar id) >>= fun ty ->
+ nothing_to_inject (Proofview.Goal.sigma gl, Proofview.Goal.env gl, ty);
+ Proofview.V82.tactic (discharge_hyp (id, (id, "")))
+ | (e,info) -> Proofview.tclZERO ~info e)
end
let injectidl2rtac id c =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index da623703a2..38b26d06b9 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -465,7 +465,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr =
Tactics.apply_type ~typecheck:true cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), sigma0
in
let cvtac' =
- Proofview.tclOR cvtac begin function
+ Proofview.tclORELSE cvtac begin function
| (PRtype_error e, _) ->
let error = Option.cata (fun (env, sigma, te) ->
Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te))
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index ad0a31622c..d99ead139d 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -150,7 +150,15 @@ let is_tac_in_term ?extra_scope { annotation; body; glob_env; interp_env } =
let sigma = sigma goal in
let ist = Ssrcommon.option_assert_get glob_env (Pp.str"not a term") in
(* We use the env of the goal, not the global one *)
- let ist = { ist with Genintern.genv } in
+ let ist =
+ let open Genintern in
+ {
+ ltacvars = ist.ast_ltacvars;
+ extra = ist.ast_extra;
+ intern_sign = ist.ast_intern_sign;
+ genv;
+ }
+ in
(* We open extra_scope *)
let body =
match extra_scope with
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:05:26 +0000