From bf7515a299d894762e10cf0f116e156073071879 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 11 Aug 2016 12:44:03 +0200 Subject: CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" function --- kernel/context.ml | 4 ---- kernel/context.mli | 2 -- 2 files changed, 6 deletions(-) (limited to 'kernel') diff --git a/kernel/context.ml b/kernel/context.ml index 2b6bc34f90..2f4997055d 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -142,10 +142,6 @@ struct match decl with | LocalAssum (n,ty) -> f ty acc | LocalDef (n,v,ty) -> f ty (f v acc) - - let of_tuple = function - | n, None, ty -> LocalAssum (n,ty) - | n, Some v, ty -> LocalDef (n,v,ty) end (** Rel-context is represented as a list of declarations. diff --git a/kernel/context.mli b/kernel/context.mli index 6fce1b95a8..55ea8921be 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -80,8 +80,6 @@ sig (** Reduce all terms in a given declaration to a single value. *) val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a - - val of_tuple : Name.t * Constr.t option * Constr.t -> t end (** Rel-context is represented as a list of declarations. -- cgit v1.2.3