1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
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)
|
