diff options
| author | msozeau | 2007-07-12 11:04:41 +0000 |
|---|---|---|
| committer | msozeau | 2007-07-12 11:04:41 +0000 |
| commit | c8df59f4e115d16fba7bb4d94ac784052f3a25d6 (patch) | |
| tree | 3778a4ee9f2b291f8eea86a5c8ced20546d9bf55 /contrib/subtac/context.ml | |
| parent | 29195517641f33bb79cf79f994917b1240fe0eaa (diff) | |
Remove dead modules in Subtac.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9973 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/context.ml')
| -rw-r--r-- | contrib/subtac/context.ml | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/contrib/subtac/context.ml b/contrib/subtac/context.ml deleted file mode 100644 index 236b0ea534..0000000000 --- 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) |
