aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml4
-rw-r--r--tactics/class_tactics.ml17
-rw-r--r--tactics/eauto.ml19
-rw-r--r--tactics/equality.ml3
-rw-r--r--tactics/hints.ml12
-rw-r--r--tactics/leminv.ml8
-rw-r--r--tactics/tactics.ml95
7 files changed, 70 insertions, 88 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index fa8435d1ff..e7e21b5f4b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -514,8 +514,8 @@ let delta_auto debug mod_delta n lems dbnames =
let delta_auto =
if Flags.profile then
- let key = Profile.declare_profile "delta_auto" in
- Profile.profile5 key delta_auto
+ let key = CProfile.declare_profile "delta_auto" in
+ CProfile.profile5 key delta_auto
else delta_auto
let auto ?(debug=Off) n = delta_auto debug false n
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index cee6d4bea7..9e4d132d4e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -376,7 +376,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
Proofview.Goal.enter
begin fun gl ->
let tacs = e_trivial_resolve db_list local_db secvars only_classes
- (project gl) (pf_concl gl) in
+ (pf_env gl) (project gl) (pf_concl gl) in
tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs)
end
in
@@ -386,7 +386,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
in
tclFIRST (List.map tclCOMPLETE tacl)
-and e_my_find_search db_list local_db secvars hdc complete only_classes sigma concl =
+and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl =
let open Proofview.Notations in
let prods, concl = EConstr.decompose_prod_assum sigma concl in
let nprods = List.length prods in
@@ -464,7 +464,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
in
let tac = run_hint t tac in
let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
- let _, env = Pfedit.get_current_context () in
let pp =
match p with
| Some pat when get_typeclasses_filtered_unification () ->
@@ -476,16 +475,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
| _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp))
in List.map tac_of_hint hintl
-and e_trivial_resolve db_list local_db secvars only_classes sigma concl =
+and e_trivial_resolve db_list local_db secvars only_classes env sigma concl =
let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in
try
- e_my_find_search db_list local_db secvars hd true only_classes sigma concl
+ e_my_find_search db_list local_db secvars hd true only_classes env sigma concl
with Not_found -> []
-let e_possible_resolve db_list local_db secvars only_classes sigma concl =
+let e_possible_resolve db_list local_db secvars only_classes env sigma concl =
let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in
try
- e_my_find_search db_list local_db secvars hd false only_classes sigma concl
+ e_my_find_search db_list local_db secvars hd false only_classes env sigma concl
with Not_found -> []
let cut_of_hints h =
@@ -719,7 +718,7 @@ module V85 = struct
let concl = Goal.V82.concl s gl in
let tacgl = {it = gl; sigma = s;} in
let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in
- let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in
+ let poss = e_possible_resolve hints info.hints secvars info.only_classes env s concl in
let unique = is_unique env s concl in
let rec aux i foundone = function
| (tac, _, extern, name, pp) :: tl ->
@@ -1072,7 +1071,7 @@ module Search = struct
else str" without backtracking"));
let secvars = compute_secvars gl in
let poss =
- e_possible_resolve hints info.search_hints secvars info.search_only_classes sigma concl in
+ e_possible_resolve hints info.search_hints secvars info.search_only_classes env sigma concl in
(* If no goal depends on the solution of this one or the
instances are irrelevant/assumed to be unique, then
we don't need to backtrack, as long as no evar appears in the goal
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index f5c6ab8799..6ea6155e0d 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -148,12 +148,12 @@ let rec e_trivial_fail_db db_list local_db =
let tacl =
registered_e_assumption ::
(Tacticals.New.tclTHEN Tactics.intro next) ::
- (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
+ (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
in
Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
end
-and e_my_find_search sigma db_list local_db secvars hdc concl =
+and e_my_find_search env sigma db_list local_db secvars hdc concl =
let hint_of_db = hintmap_of sigma secvars hdc concl in
let hintl =
List.map_append (fun db ->
@@ -178,20 +178,19 @@ and e_my_find_search sigma db_list local_db secvars hdc concl =
| Extern tacast -> conclPattern concl p tacast
in
let tac = run_hint t tac in
- let sigma, env = Pfedit.get_current_context () in
(tac, lazy (pr_hint env sigma t)))
in
List.map tac_of_hint hintl
-and e_trivial_resolve sigma db_list local_db secvars gl =
+and e_trivial_resolve env sigma db_list local_db secvars gl =
let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
- try priority (e_my_find_search sigma db_list local_db secvars hd gl)
+ try priority (e_my_find_search env sigma db_list local_db secvars hd gl)
with Not_found -> []
-let e_possible_resolve sigma db_list local_db secvars gl =
+let e_possible_resolve env sigma db_list local_db secvars gl =
let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
try List.map (fun (b, (tac, pp)) -> (tac, b, pp))
- (e_my_find_search sigma db_list local_db secvars hd gl)
+ (e_my_find_search env sigma db_list local_db secvars hd gl)
with Not_found -> []
let find_first_goal gls =
@@ -291,7 +290,7 @@ module SearchProblem = struct
let l =
let concl = Reductionops.nf_evar (project g) (pf_concl g) in
filter_tactics s.tacres
- (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
+ (e_possible_resolve (pf_env g) (project g) s.dblist (List.hd s.localdb) secvars concl)
in
List.map
(fun (lgls, cost, pp) ->
@@ -405,8 +404,8 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
pr_info_nop d;
user_err Pp.(str "eauto: search failed")
-(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *)
-(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *)
+(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *)
+(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *)
let eauto_with_bases ?(debug=Off) np lems db_list =
tclTRY (e_search_auto debug np lems db_list)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0d6263246e..22073d39b6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1436,8 +1436,9 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
(tac (clenv_value eq_clause))
let get_previous_hyp_position id gl =
+ let env, sigma = Proofview.Goal.(env gl, sigma gl) in
let rec aux dest = function
- | [] -> raise (RefinerError (NoSuchHyp id))
+ | [] -> raise (RefinerError (env, sigma, NoSuchHyp id))
| d :: right ->
let hyp = Context.Named.Declaration.get_id d in
if Id.equal hyp id then dest else aux (MoveAfter hyp) right
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 70e84013ba..7f9b5ef34e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1400,15 +1400,10 @@ let pr_hint env sigma h = match h.obj with
| Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c)
| Res_pf_THEN_trivial_fail (c, _) ->
(str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial")
- | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c)
+ | Unfold_nth c ->
+ str"unfold " ++ pr_evaluable_reference c
| Extern tac ->
- let env =
- try
- let (_, env) = Pfedit.get_current_goal_context () in
- env
- with e when CErrors.noncritical e -> Global.env ()
- in
- (str "(*external*) " ++ Pputils.pr_glb_generic env tac)
+ str "(*external*) " ++ Pputils.pr_glb_generic env tac
let pr_id_hint env sigma (id, v) =
let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in
@@ -1507,6 +1502,7 @@ let pr_hint_db_env env sigma db =
hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++
content
+(* Deprecated in the mli *)
let pr_hint_db db =
let sigma, env = Pfedit.get_current_context () in
pr_hint_db_env env sigma db
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1ae3577edb..01065868d4 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -249,11 +249,11 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
let add_inversion_lemma_exn na com comsort bool tac =
let env = Global.env () in
- let evd = ref (Evd.from_env env) in
- let c = Constrintern.interp_type_evars env evd com in
- let evd, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env !evd comsort in
+ let sigma = Evd.from_env env in
+ let sigma, c = Constrintern.interp_type_evars env sigma com in
+ let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in
try
- add_inversion_lemma na env evd c sort bool tac
+ add_inversion_lemma na env sigma c sort bool tac
with
| UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
user_err ~hdr:"Inv needs Nodep Prop Set" s
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e072bd95f6..508040ec18 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -59,28 +59,6 @@ let typ_of env sigma c =
open Goptions
-(* Option for 8.2 compatibility *)
-let dependent_propositions_elimination = ref true
-
-let use_dependent_propositions_elimination () =
- !dependent_propositions_elimination
-
-let _ =
- declare_bool_option
- { optdepr = true; (* remove in 8.8 *)
- optname = "dependent-propositions-elimination tactic";
- optkey = ["Dependent";"Propositions";"Elimination"];
- optread = (fun () -> !dependent_propositions_elimination) ;
- optwrite = (fun b -> dependent_propositions_elimination := b) }
-
-let _ =
- declare_bool_option
- { optdepr = true; (* remove in 8.8 *)
- optname = "trigger bugged context matching compatibility";
- optkey = ["Tactic";"Compat";"Context"];
- optread = (fun () -> !Flags.tactic_context_compat) ;
- optwrite = (fun b -> Flags.tactic_context_compat := b) }
-
let apply_solve_class_goals = ref false
let _ =
@@ -187,7 +165,7 @@ let introduction ?(check=true) id =
match EConstr.kind sigma concl with
| Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
| LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
- | _ -> raise (RefinerError IntroNeedsProduct)
+ | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct))
end
let refine = Tacmach.refine
@@ -319,7 +297,7 @@ let move_hyp id dest =
let ty = Proofview.Goal.concl gl in
let store = Proofview.Goal.extra gl in
let sign = named_context_val env in
- let sign' = move_hyp_in_named_context sigma id dest sign in
+ let sign' = move_hyp_in_named_context env sigma id dest sign in
let env = reset_with_named_context sign' env in
Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true ~store ty
@@ -348,13 +326,15 @@ let rename_hyp repl =
let hyps = Proofview.Goal.hyps gl in
let concl = Proofview.Goal.concl gl in
let store = Proofview.Goal.extra gl in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
(** Check that we do not mess variables *)
let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in
let vars = List.fold_left fold Id.Set.empty hyps in
let () =
if not (Id.Set.subset src vars) then
let hyp = Id.Set.choose (Id.Set.diff src vars) in
- raise (RefinerError (NoSuchHyp hyp))
+ raise (RefinerError (env, sigma, NoSuchHyp hyp))
in
let mods = Id.Set.diff vars src in
let () =
@@ -442,9 +422,9 @@ let find_name mayrepl decl naming gl = match naming with
(* Computing position of hypotheses for replacing *)
(**************************************************************)
-let get_next_hyp_position id =
+let get_next_hyp_position env sigma id =
let rec aux = function
- | [] -> error_no_such_hypothesis id
+ | [] -> error_no_such_hypothesis env sigma id
| decl :: right ->
if Id.equal (NamedDecl.get_id decl) id then
match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst
@@ -453,9 +433,9 @@ let get_next_hyp_position id =
in
aux
-let get_previous_hyp_position id =
+let get_previous_hyp_position env sigma id =
let rec aux dest = function
- | [] -> error_no_such_hypothesis id
+ | [] -> error_no_such_hypothesis env sigma id
| decl :: right ->
let hyp = NamedDecl.get_id decl in
if Id.equal hyp id then dest else aux (MoveAfter hyp) right
@@ -483,7 +463,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
let sign = named_context_val env in
let sign',t,concl,sigma =
if replace then
- let nexthyp = get_next_hyp_position id (named_context_of_val sign) in
+ let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in
sign',t,concl,sigma
@@ -1000,6 +980,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
+ let env = Tacmach.New.pf_env gl in
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
match EConstr.kind sigma concl with
| Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
@@ -1009,7 +990,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
let name = find_name false (LocalDef (name,b,t)) name_flag gl in
build_intro_tac name move_flag tac
| _ ->
- begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct)
+ begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct))
(* Note: red_in_concl includes betaiotazeta and this was like *)
(* this since at least V6.3 (a pity *)
(* that intro do betaiotazeta only when reduction is needed; and *)
@@ -1020,7 +1001,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
(Tacticals.New.tclTHEN hnf_in_concl
(intro_then_gen name_flag move_flag false dep_flag tac))
begin function (e, info) -> match e with
- | RefinerError IntroNeedsProduct ->
+ | RefinerError (env, sigma, IntroNeedsProduct) ->
Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
| e -> Proofview.tclZERO ~info e
end
@@ -1059,7 +1040,7 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
(fun id -> aux (n+1) (id::ids))
end
begin function (e, info) -> match e with
- | RefinerError IntroNeedsProduct ->
+ | RefinerError (env, sigma, IntroNeedsProduct) ->
tac ids
| e -> Proofview.tclZERO ~info e
end
@@ -1070,8 +1051,9 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
let intro_replacing id =
Proofview.Goal.enter begin fun gl ->
+ let env, sigma = Proofview.Goal.(env gl, sigma gl) in
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
- let next_hyp = get_next_hyp_position id hyps in
+ let next_hyp = get_next_hyp_position env sigma id hyps in
Tacticals.New.tclTHENLIST [
clear_for_replacing [id];
introduction id;
@@ -1090,8 +1072,9 @@ let intro_replacing id =
let intros_possibly_replacing ids =
let suboptimal = true in
Proofview.Goal.enter begin fun gl ->
+ let env, sigma = Proofview.Goal.(env gl, sigma gl) in
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
- let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in
+ let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in
Tacticals.New.tclTHEN
(Tacticals.New.tclMAP (fun id ->
Tacticals.New.tclTRY (clear_for_replacing [id]))
@@ -1105,7 +1088,8 @@ let intros_possibly_replacing ids =
let intros_replacing ids =
Proofview.Goal.enter begin fun gl ->
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
- let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in
+ let env, sigma = Proofview.Goal.(env gl, sigma gl) in
+ let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in
Tacticals.New.tclTHEN
(clear_for_replacing ids)
(Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
@@ -1976,11 +1960,11 @@ let cut_and_apply c =
(* Exact tactics *)
(********************************************************************)
-(* let convert_leqkey = Profile.declare_profile "convert_leq";; *)
-(* let convert_leq = Profile.profile3 convert_leqkey convert_leq *)
+(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *)
+(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *)
-(* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *)
-(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
+(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *)
+(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *)
let exact_no_check c =
Refine.refine ~typecheck:false (fun h -> (h,c))
@@ -2633,8 +2617,10 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
Proofview.Goal.enter begin fun gl ->
let destopt =
if with_evars then MoveLast (* evars would depend on the whole context *)
- else
- get_previous_hyp_position id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) in
+ else (
+ let env, sigma = Proofview.Goal.(env gl, sigma gl) in
+ get_previous_hyp_position env sigma id (Proofview.Goal.hyps (Proofview.Goal.assume gl))
+ ) in
let naming,ipat_tac =
prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in
let lemmas_target, last_lemma_target =
@@ -4141,8 +4127,7 @@ let guess_elim isrec dep s hyp0 gl =
let env = Tacmach.New.pf_env gl in
let sigma = Tacmach.New.project gl in
let u = EInstance.kind (Tacmach.New.project gl) u in
- if use_dependent_propositions_elimination () && dep = Some true
- then
+ if dep then
let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in
let ind = EConstr.of_constr ind in
(sigma, ind)
@@ -4174,11 +4159,10 @@ let find_induction_type isrec elim hyp0 gl =
match elim with
| None ->
let sort = Tacticals.New.elimination_sort_of_goal gl in
- let _, (elimc,elimt),_ =
- guess_elim isrec None sort hyp0 gl in
- let scheme = compute_elim_sig sigma ~elimc elimt in
- (* We drop the scheme waiting to know if it is dependent *)
- scheme, ElimOver (isrec,hyp0)
+ let _, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in
+ let scheme = compute_elim_sig sigma ~elimc elimt in
+ (* We drop the scheme waiting to know if it is dependent *)
+ scheme, ElimOver (isrec,hyp0)
| Some e ->
let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
let scheme = compute_elim_sig sigma ~elimc elimt in
@@ -4209,7 +4193,7 @@ let get_eliminator elim dep s gl =
| ElimUsing (elim,indsign) ->
Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign
| ElimOver (isrec,id) ->
- let evd, (elimc,elimt),_ as elims = guess_elim isrec (Some dep) s id gl in
+ let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
let _, (l, s) = compute_elim_signature elims id in
let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d)))
(List.rev s.branches)
@@ -4448,8 +4432,11 @@ let check_enough_applied env sigma elim =
check_expected_type env sigma elimc elimt
let guard_no_unifiable = Proofview.guard_no_unifiable >>= function
-| None -> Proofview.tclUNIT ()
-| Some l -> Proofview.tclZERO (RefinerError (UnresolvedBindings l))
+ | None -> Proofview.tclUNIT ()
+ | Some l ->
+ Proofview.tclENV >>= function env ->
+ Proofview.tclEVARMAP >>= function sigma ->
+ Proofview.tclZERO (RefinerError (env, sigma, UnresolvedBindings l))
let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac =
@@ -4648,7 +4635,7 @@ let induction_destruct isrec with_evars (lc,elim) =
(Tacticals.New.tclMAP (fun (a,b,cl) ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
+ let sigma = Tacmach.New.project gl in
onOpenInductionArg env sigma (fun clear_flag a ->
induction_gen clear_flag false with_evars None (a,b) cl) a
end) l)
@@ -4673,7 +4660,7 @@ let induction_destruct isrec with_evars (lc,elim) =
end
let induction ev clr c l e =
- induction_gen clr true ev e
+ induction_gen clr true ev e
((Evd.empty,(c,NoBindings)),(None,l)) None
let destruct ev clr c l e =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 07:03:51 +0000