Remove fterm internals from the CClosure API.

SkySkimmer · Dec 19, 2024 · 9d01c8e · 9d01c8e
1 parent a158888
commit 9d01c8e
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 9 deletions.
diff --git 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
@@ -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