blob: 88afec14d58edac48c21c95a811f3b5b4bc0a9fc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* A more advanced example of how to explore the structure of terms of
type constr is given in the coq-dpdgraph plugin. *)
let simple_body_access gref =
let open Names.GlobRef in
match gref with
| VarRef _ ->
failwith "variables are not covered in this example"
| IndRef _ ->
failwith "inductive types are not covered in this example"
| ConstructRef _ ->
failwith "constructors are not covered in this example"
| ConstRef cst ->
let cb = Environ.lookup_constant cst (Global.env()) in
match Global.body_of_constant_body Library.indirect_accessor cb with
| Some(e, _, _) -> EConstr.of_constr e
| None -> failwith "This term has no value"
|
