summaryrefslogtreecommitdiff
path: root/contrib/first-order
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/first-order')
-rw-r--r--contrib/first-order/formula.ml10
-rw-r--r--contrib/first-order/formula.mli2
-rw-r--r--contrib/first-order/g_ground.ml423
-rw-r--r--contrib/first-order/ground.ml15
-rw-r--r--contrib/first-order/ground.mli2
-rw-r--r--contrib/first-order/instances.ml27
-rw-r--r--contrib/first-order/instances.mli2
-rw-r--r--contrib/first-order/rules.ml44
-rw-r--r--contrib/first-order/rules.mli4
-rw-r--r--contrib/first-order/sequent.ml16
-rw-r--r--contrib/first-order/sequent.mli2
-rw-r--r--contrib/first-order/unify.ml6
-rw-r--r--contrib/first-order/unify.mli2
13 files changed, 77 insertions, 78 deletions
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 49cb8e25..fde48d2b 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: formula.ml,v 1.18.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: formula.ml 7493 2005-11-02 22:12:16Z mohring $ *)
open Hipattern
open Names
@@ -47,14 +47,14 @@ let rec nb_prod_after n c=
let construct_nhyps ind gls =
let env=pf_env gls in
- let nparams = (snd (Global.lookup_inductive ind)).mind_nparams in
- let constr_types = Inductive.arities_of_constructors (pf_env gls) ind in
+ let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+ let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in
let hyp = nb_prod_after nparams in
Array.map hyp constr_types
(* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
let ind_hyps nevar ind largs gls=
- let types= Inductive.arities_of_constructors (pf_env gls) ind in
+ let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
let lp=Array.length types in
let myhyps i=
let t1=Term.prod_applist types.(i) largs in
@@ -99,7 +99,7 @@ let rec kind_of_formula gl term =
let has_realargs=(n>0) in
let is_trivial=
let is_constant c =
- nb_prod c = mip.mind_nparams in
+ nb_prod c = mib.mind_nparams in
array_exists is_constant mip.mind_nf_lc in
if Inductiveops.mis_is_recursive (ind,mib,mip) ||
(has_realargs && not is_trivial)
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index db24f20f..8703045c 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: formula.mli,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: formula.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
open Term
open Names
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index f85f2171..0970d5db 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_ground.ml4,v 1.10.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: g_ground.ml4 7909 2006-01-21 11:09:18Z herbelin $ *)
open Formula
open Sequent
@@ -41,7 +41,7 @@ let _=
let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
-let fail_solver=tclFAIL 0 "GTauto failed"
+let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
type external_env=
Ids of global_reference list
@@ -81,23 +81,16 @@ let normalize_evaluables=
unfold_in_hyp (Lazy.force defined_connectives)
(Tacexpr.InHypType id)) *)
-TACTIC EXTEND Firstorder
- [ "Firstorder" tactic_opt(t) "with" ne_reference_list(l) ] ->
+TACTIC EXTEND firstorder
+ [ "firstorder" tactic_opt(t) "with" ne_reference_list(l) ] ->
[ gen_ground_tac true (option_app eval_tactic t) (Ids l) ]
-| [ "Firstorder" tactic_opt(t) "using" ne_preident_list(l) ] ->
+| [ "firstorder" tactic_opt(t) "using" ne_preident_list(l) ] ->
[ gen_ground_tac true (option_app eval_tactic t) (Bases l) ]
-| [ "Firstorder" tactic_opt(t) ] ->
+| [ "firstorder" tactic_opt(t) ] ->
[ gen_ground_tac true (option_app eval_tactic t) Void ]
END
-(* Obsolete since V8.0
-TACTIC EXTEND GTauto
- [ "GTauto" ] ->
- [ gen_ground_tac false (Some fail_solver) Void ]
-END
-*)
-
-TACTIC EXTEND GIntuition
- [ "GIntuition" tactic_opt(t) ] ->
+TACTIC EXTEND gintuition
+ [ "gintuition" tactic_opt(t) ] ->
[ gen_ground_tac false (option_app eval_tactic t) Void ]
END
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 23e27a3c..bb096308 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ground.ml,v 1.5.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: ground.ml 7909 2006-01-21 11:09:18Z herbelin $ *)
open Formula
open Sequent
@@ -45,23 +45,23 @@ let update_flags ()=
*)
let update_flags ()=
- let predref=ref Names.KNpred.empty in
+ let predref=ref Names.Cpred.empty in
let f coe=
try
let kn=destConst (Classops.get_coercion_value coe) in
- predref:=Names.KNpred.add kn !predref
+ predref:=Names.Cpred.add kn !predref
with Invalid_argument "destConst"-> () in
List.iter f (Classops.coercions ());
red_flags:=
Closure.RedFlags.red_add_transparent
Closure.betaiotazeta
- (Names.Idpred.full,Names.KNpred.complement !predref)
+ (Names.Idpred.full,Names.Cpred.complement !predref)
let ground_tac solver startseq gl=
update_flags ();
let rec toptac skipped seq gl=
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
- then Pp.msgnl (Proof_trees.pr_goal (sig_it gl));
+ then Pp.msgnl (Printer.pr_goal (sig_it gl));
tclORELSE (axiom_tac seq.gl seq)
begin
try
@@ -78,7 +78,7 @@ let ground_tac solver startseq gl=
| Rforall->
let backtrack1=
if !qflag then
- tclFAIL 0 "reversible in 1st order mode"
+ tclFAIL 0 (Pp.str "reversible in 1st order mode")
else
backtrack in
forall_tac backtrack continue (re_add seq1)
@@ -117,7 +117,8 @@ let ground_tac solver startseq gl=
backtrack2 (* need special backtracking *)
| Lexists ind ->
if !qflag then
- left_exists_tac ind hd.id continue (re_add seq1)
+ left_exists_tac ind backtrack hd.id
+ continue (re_add seq1)
else backtrack
| LA (typ,lap)->
let la_tac=
diff --git a/contrib/first-order/ground.mli b/contrib/first-order/ground.mli
index cfc17e77..621f99db 100644
--- a/contrib/first-order/ground.mli
+++ b/contrib/first-order/ground.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ground.mli,v 1.1.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: ground.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
val ground_tac: Tacmach.tactic ->
(Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index e2e9e2ef..254d7b84 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: instances.ml,v 1.9.2.1 2004/07/16 19:30:10 herbelin Exp $ i*)
+(*i $Id: instances.ml 8654 2006-03-22 15:36:58Z msozeau $ i*)
open Formula
open Sequent
@@ -105,10 +105,10 @@ let dummy_bvid=id_of_string "x"
let mk_open_instance id gl m t=
let env=pf_env gl in
- let evmap=Refiner.sig_sig gl in
+ let evmap=Refiner.project gl in
let var_id=
if id==dummy_id then dummy_bvid else
- let typ=pf_type_of gl (constr_of_reference id) in
+ let typ=pf_type_of gl (constr_of_global id) in
(* since we know we will get a product,
reduction is not too expensive *)
let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
@@ -121,15 +121,18 @@ let mk_open_instance id gl m t=
let nid=(fresh_id avoid var_id gl) in
(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
let nt=it_mkLambda_or_LetIn revt (aux m []) in
- let rawt=Detyping.detype (false,env) [] [] nt in
+ let rawt=Detyping.detype false [] [] nt in
let rec raux n t=
if n=0 then t else
match t with
RLambda(loc,name,_,t0)->
let t1=raux (n-1) t0 in
- RLambda(loc,name,RHole (dummy_loc,BinderType name),t1)
+ RLambda(loc,name,RHole (dummy_loc,Evd.BinderType name),t1)
| _-> anomaly "can't happen" in
- let ntt=Pretyping.understand evmap env (raux m rawt) in
+ let ntt=try
+ Pretyping.Default.understand evmap env (raux m rawt)
+ with _ ->
+ error "Untypable instance, maybe higher-order non-prenex quantification" in
Sign.decompose_lam_n_assum m ntt
(* tactics *)
@@ -138,13 +141,13 @@ let left_instance_tac (inst,id) continue seq=
match inst with
Phantom dom->
if lookup (id,None) seq then
- tclFAIL 0 "already done"
+ tclFAIL 0 (Pp.str "already done")
else
tclTHENS (cut dom)
[tclTHENLIST
[introf;
(fun gls->generalize
- [mkApp(constr_of_reference id,
+ [mkApp(constr_of_global id,
[|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
introf;
tclSOLVE [wrap 1 false continue
@@ -152,7 +155,7 @@ let left_instance_tac (inst,id) continue seq=
tclTRY assumption]
| Real((m,t) as c,_)->
if lookup (id,Some c) seq then
- tclFAIL 0 "already done"
+ tclFAIL 0 (Pp.str "already done")
else
let special_generalize=
if m>0 then
@@ -160,10 +163,10 @@ let left_instance_tac (inst,id) continue seq=
let (rc,ot)= mk_open_instance id gl m t in
let gt=
it_mkLambda_or_LetIn
- (mkApp(constr_of_reference id,[|ot|])) rc in
+ (mkApp(constr_of_global id,[|ot|])) rc in
generalize [gt] gl
else
- generalize [mkApp(constr_of_reference id,[|t|])]
+ generalize [mkApp(constr_of_global id,[|t|])]
in
tclTHENLIST
[special_generalize;
@@ -186,7 +189,7 @@ let right_instance_tac inst continue seq=
(tclTHEN (split (Rawterm.ImplicitBindings [t]))
(tclSOLVE [wrap 0 true continue (deepen seq)]))
| Real ((m,t),_) ->
- tclFAIL 0 "not implemented ... yet"
+ tclFAIL 0 (Pp.str "not implemented ... yet")
let instance_tac inst=
if (snd inst)==dummy_id then
diff --git a/contrib/first-order/instances.mli b/contrib/first-order/instances.mli
index 509bfc70..7667c89f 100644
--- a/contrib/first-order/instances.mli
+++ b/contrib/first-order/instances.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: instances.mli,v 1.3.2.1 2004/07/16 19:30:10 herbelin Exp $ i*)
+(*i $Id: instances.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
open Term
open Tacmach
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 7fbefa37..f6653b82 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rules.ml,v 1.24.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: rules.ml 7909 2006-01-21 11:09:18Z herbelin $ *)
open Util
open Names
@@ -57,18 +57,18 @@ let clear_global=function
(* connection rules *)
let axiom_tac t seq=
- try exact_no_check (constr_of_reference (find_left t seq))
- with Not_found->tclFAIL 0 "No axiom link"
+ try exact_no_check (constr_of_global (find_left t seq))
+ with Not_found->tclFAIL 0 (Pp.str "No axiom link")
let ll_atom_tac a backtrack id continue seq=
tclIFTHENELSE
(try
tclTHENLIST
- [generalize [mkApp(constr_of_reference id,
- [|constr_of_reference (find_left a seq)|])];
+ [generalize [mkApp(constr_of_global id,
+ [|constr_of_global (find_left a seq)|])];
clear_global id;
intro]
- with Not_found->tclFAIL 0 "No link")
+ with Not_found->tclFAIL 0 (Pp.str "No link"))
(wrap 1 false continue seq) backtrack
(* right connectives rules *)
@@ -92,7 +92,7 @@ let left_and_tac ind backtrack id continue seq gls=
let n=(construct_nhyps ind gls).(0) in
tclIFTHENELSE
(tclTHENLIST
- [simplest_elim (constr_of_reference id);
+ [simplest_elim (constr_of_global id);
clear_global id;
tclDO n intro])
(wrap n false continue seq)
@@ -106,12 +106,12 @@ let left_or_tac ind backtrack id continue seq gls=
tclDO n intro;
wrap n false continue seq] in
tclIFTHENSVELSE
- (simplest_elim (constr_of_reference id))
+ (simplest_elim (constr_of_global id))
(Array.map f v)
backtrack gls
let left_false_tac id=
- simplest_elim (constr_of_reference id)
+ simplest_elim (constr_of_global id)
(* left arrow connective rules *)
@@ -127,7 +127,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in
let vars=Array.init p (fun j->mkRel (p-j)) in
let capply=mkApp ((lift p cstr),vars) in
- let head=mkApp ((lift p (constr_of_reference id)),[|capply|]) in
+ let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
Sign.it_mkLambda_or_LetIn head rc in
let lp=Array.length rcs in
let newhyps=list_tabulate myterm lp in
@@ -141,7 +141,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
let ll_arrow_tac a b c backtrack id continue seq=
let cc=mkProd(Anonymous,a,(lift 1 b)) in
let d=mkLambda (Anonymous,b,
- mkApp ((constr_of_reference id),
+ mkApp ((constr_of_global id),
[|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
tclORELSE
(tclTHENS (cut c)
@@ -150,7 +150,7 @@ let ll_arrow_tac a b c backtrack id continue seq=
clear_global id;
wrap 1 false continue seq];
tclTHENS (cut cc)
- [exact_no_check (constr_of_reference id);
+ [exact_no_check (constr_of_global id);
tclTHENLIST
[generalize [d];
clear_global id;
@@ -168,17 +168,19 @@ let forall_tac backtrack continue seq=
(tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
backtrack))
(if !qflag then
- tclFAIL 0 "reversible in 1st order mode"
+ tclFAIL 0 (Pp.str "reversible in 1st order mode")
else
backtrack)
-let left_exists_tac ind id continue seq gls=
+let left_exists_tac ind backtrack id continue seq gls=
let n=(construct_nhyps ind gls).(0) in
- tclTHENLIST
- [simplest_elim (constr_of_reference id);
- clear_global id;
- tclDO n intro;
- (wrap (n-1) false continue seq)] gls
+ tclIFTHENELSE
+ (simplest_elim (constr_of_global id))
+ (tclTHENLIST [clear_global id;
+ tclDO n intro;
+ (wrap (n-1) false continue seq)])
+ backtrack
+ gls
let ll_forall_tac prod backtrack id continue seq=
tclORELSE
@@ -187,7 +189,7 @@ let ll_forall_tac prod backtrack id continue seq=
[intro;
(fun gls->
let id0=pf_nth_hyp_id gls 1 in
- let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in
+ let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
tclTHEN (generalize [term]) (clear [id0]) gls);
clear_global id;
intro;
@@ -211,4 +213,4 @@ let normalize_evaluables=
None->unfold_in_concl (Lazy.force defined_connectives)
| Some (id,_,_)->
unfold_in_hyp (Lazy.force defined_connectives)
- (id,[],(Tacexpr.InHypTypeOnly,ref None)))
+ (id,[],Tacexpr.InHypTypeOnly))
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index eb4d81bd..3798d8d4 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rules.mli,v 1.11.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: rules.mli 6141 2004-09-27 14:55:34Z corbinea $ *)
open Term
open Tacmach
@@ -47,7 +47,7 @@ val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking
val forall_tac : seqtac with_backtracking
-val left_exists_tac : inductive -> lseqtac
+val left_exists_tac : inductive -> lseqtac with_backtracking
val ll_forall_tac : types -> lseqtac with_backtracking
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 13215348..805700b0 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: sequent.ml,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: sequent.ml 7925 2006-01-24 23:20:39Z herbelin $ *)
open Term
open Util
@@ -91,8 +91,8 @@ let compare_constr_int f t1 t2 =
| Meta m1, Meta m2 -> m1 - m2
| Var id1, Var id2 -> Pervasives.compare id1 id2
| Sort s1, Sort s2 -> Pervasives.compare s1 s2
- | Cast (c1,_), _ -> f c1 t2
- | _, Cast (c2,_) -> f t1 c2
+ | Cast (c1,_,_), _ -> f c1 t2
+ | _, Cast (c2,_,_) -> f t1 c2
| Prod (_,t1,c1), Prod (_,t2,c2)
| Lambda (_,t1,c1), Lambda (_,t2,c2) ->
(f =? f) t1 t2 c1 c2
@@ -255,7 +255,7 @@ let empty_seq depth=
let create_with_ref_list l depth gl=
let f gr seq=
- let c=constr_of_reference gr in
+ let c=constr_of_global gr in
let typ=(pf_type_of gl c) in
add_formula Hyp gr typ seq gl in
List.fold_right f l (empty_seq depth)
@@ -269,7 +269,7 @@ let create_with_auto_hints l depth gl=
Res_pf (c,_) | Give_exact c
| Res_pf_THEN_trivial_fail (c,_) ->
(try
- let gr=reference_of_constr c in
+ let gr=global_of_constr c in
let typ=(pf_type_of gl c) in
seqref:=add_formula Hint gr typ !seqref gl
with Not_found->())
@@ -278,7 +278,7 @@ let create_with_auto_hints l depth gl=
let h dbname=
let hdb=
try
- Util.Stringmap.find dbname !searchtable
+ searchtable_map dbname
with Not_found->
error ("Firstorder: "^dbname^" : No such Hint database") in
Hint_db.iter g hdb in
@@ -289,9 +289,9 @@ let print_cmap map=
let print_entry c l s=
let xc=Constrextern.extern_constr false (Global.env ()) c in
str "| " ++
- Util.prlist (Ppconstr.pr_global Idset.empty) l ++
+ Util.prlist Printer.pr_global l ++
str " : " ++
- Ppconstr.pr_constr xc ++
+ Ppconstr.pr_constr_expr xc ++
cut () ++
s in
msgnl (v 0
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
index df27d2ff..47fb74c7 100644
--- a/contrib/first-order/sequent.mli
+++ b/contrib/first-order/sequent.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: sequent.mli,v 1.8.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: sequent.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
open Term
open Util
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index 1186fb90..1dd13cbe 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: unify.ml,v 1.10.2.1 2004/07/16 19:30:10 herbelin Exp $ i*)
+(*i $Id: unify.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
open Util
open Formula
@@ -59,8 +59,8 @@ let unif t1 t2=
if Intset.is_empty (free_rels t) &&
not (occur_term (mkMeta i) t) then
bind i t else raise (UFAIL(nt1,nt2))
- | Cast(_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
- | _,Cast(_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
+ | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
+ | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
| (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
| Case (_,pa,ca,va),Case (_,pb,cb,vb)->
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
index dd9dbdec..9fbe3dda 100644
--- a/contrib/first-order/unify.mli
+++ b/contrib/first-order/unify.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unify.mli,v 1.7.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: unify.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
open Term
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 14:32:44 +0000