From 9d01c8eab7eadf5ab7341d6137078f77d811bde9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 12 Dec 2024 18:28:53 +0100 Subject: [PATCH] Remove fterm internals from the CClosure API. --- kernel/cClosure.ml | 3 --- kernel/cClosure.mli | 6 ------ 2 files changed, 9 deletions(-) diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index f4d3af6a473b..6a4e99a4325d 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -114,9 +114,6 @@ let get_invert fiv = fiv let fterm_of v = v.term let set_ntrl v = v.mark <- Ntrl -let mk_atom c = {mark=Ntrl;term=FAtom c} -let mk_red f = {mark=Red;term=f} - (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) let update v1 mark t = diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 5391647a0498..01c66665c2b3 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -108,12 +108,6 @@ val inject : constr -> fconstr val mk_clos : usubs -> constr -> fconstr val mk_clos_vect : usubs -> constr array -> fconstr array -(** mk_atom: prevents a term from being evaluated *) -val mk_atom : constr -> fconstr - -(** mk_red: makes a reducible term (used in ring) *) -val mk_red : fterm -> fconstr - val zip : fconstr -> stack -> fconstr val fterm_of : fconstr -> fterm