| C.Var _
| C.Meta _
| C.Sort _
- | C.Implicit
+ | C.Implicit _
| C.Cast _ -> []
| C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
| C.Prod _ -> []
let term = Hashtbl.find ids_to_terms id in
let context = get_context ids_to_terms ids_to_father_ids id in
let metasenv =
- match !P.proof with
+ match P.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
let term = Hashtbl.find ids_to_terms id in
let context = get_context ids_to_terms ids_to_father_ids id in
let metasenv =
- match !P.proof with
+ match P.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in