1 files changed, 0 insertions, 35 deletions
diff --git a/contrib/subtac/context.ml b/contrib/subtac/context.ml
deleted file mode 100644
index 236b0ea5..00000000
--- a/contrib/subtac/context.ml
+++ /dev/null
@@ -1,35 +0,0 @@
-open Term
-open Names
-
-type t = rel_declaration list (* name, optional coq interp, algorithmic type *)
-
-let assoc n t = 
-  let _, term, typ = List.find (fun (x, _, _) -> x = n) t in
-    term, typ
-
-let assoc_and_index x l =
-  let rec aux i = function
-      (y, term, typ) :: tl -> if x = y then i, term, typ else aux (succ i) tl
-    | [] -> raise Not_found
-  in aux 0 l
-
-let id_of_name = function
-    Name id -> id
-  | Anonymous -> raise (Invalid_argument "id_of_name")
-(*
-
-let subst_ctx ctx c = 
-  let rec aux ((ctx, n, c) as acc) = function
-      (name, None, typ) :: tl -> 
-	aux (((id_of_name name, None, rel_to_vars ctx typ) :: ctx), 
-	     pred n, c) tl
-    | (name, Some term, typ) :: tl ->
-	let t' = Term.substnl [term] n c in
-	  aux (ctx, n, t') tl
-    | [] -> acc
-  in 
-  let (x, _, z) = aux ([], pred (List.length ctx), c) (List.rev ctx) in 
-    (x, rel_to_vars x z)
-*)
-
-let subst_env env c = (env, c)