| 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 _ -> []
| C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
| C.Lambda _ -> []
- | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def s)]
+ | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def (s,None))]
| C.LetIn _ -> []
| C.Appl _
| C.Const _ -> []
let counter = ref 0 in
List.rev_map
(function (name,_,ty,bo) ->
- let res = Some (C.Name name, (C.Def (C.Fix (!counter,ifl)))) in
+ let res =
+ Some (C.Name name, (C.Def ((C.Fix (!counter,ifl)), Some ty)))
+ in
incr counter ;
res
) ifl
let counter = ref 0 in
List.rev_map
(function (name,ty,bo) ->
- let res = Some (C.Name name,(C.Def (C.CoFix (!counter,ifl)))) in
+ let res =
+ Some (C.Name name,(C.Def ((C.CoFix (!counter,ifl)), Some ty)))
+ in
incr counter ;
res
) ifl
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 ty = CicTypeChecker.type_of_aux' metasenv context term in
- P.perforate context term ty (* P.perforate also sets the goal *)
+ let ty,_ = (* TASSI: FIXME ehhmmmm *)
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+ in
+ P.perforate context term ty (* P.perforate also sets the goal *)
;;
exception FocusOnlyOnMeta;;
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 ty = CicTypeChecker.type_of_aux' metasenv context term in
- match term with
- Cic.Meta (n,_) -> P.goal := Some n
- | _ -> raise FocusOnlyOnMeta
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+ in
+ match term with
+ Cic.Meta (n,_) -> P.goal := Some n
+ | _ -> raise FocusOnlyOnMeta
;;