let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
C.Var (uri,exp_named_subst')
| C.Meta (n,l) ->
- let (_,canonical_context,_) =
- List.find (function (m,_,_) -> n = m) metasenv
- in
- let l' =
+ let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
+ let l' =
List.map2
(fun ct t ->
match (ct, t) with
(match l' with
[] -> assert false
| he::tl ->
- let ty = CicTypeChecker.type_of_aux' metasenv context he in
- fix_according_to_type ty he tl
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context he
+ CicUniv.empty_ugraph
+ in
+ fix_according_to_type ty he tl
(*
C.Const(uri,exp_named_subst)::l'' ->
let constant_type =
(match CicEnvironment.get_obj uri with
C.Constant (_,_,ty,_) -> ty
| C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof
+ | C.CurrentProof (_,_,_,_,params) -> raise ReferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
) in
fix_according_to_type
let term' = eta_fix' context term in
let patterns' = List.map (eta_fix' context) patterns in
let inductive_types,noparams =
- (match CicEnvironment.get_obj uri with
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
| Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,n) -> l,n
+ | Cic.InductiveDefinition (l,_,n,_) -> l,n
) in
let (_,_,_,constructors) = List.nth inductive_types tyno in
let constructor_types =
if noparams = 0 then
List.map (fun (_,t) -> t) constructors
else
- let term_type =
- CicTypeChecker.type_of_aux' metasenv context term
- in
+ let term_type,_ =
+ CicTypeChecker.type_of_aux' metasenv context term
+ CicUniv.empty_ugraph
+ in
(match term_type with
C.Appl (hd::params) ->
let rec first_n n l =
(fun newsubst (uri,t) ->
let t' = eta_fix' context t in
let ty =
- match CicEnvironment.get_obj uri with
- Cic.Variable (_,_,ty,_) -> CicSubstitution.subst_vars newsubst ty
- | _ -> raise ReferenceToNonVariable in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o with
+ Cic.Variable (_,_,ty,_,_) ->
+ CicSubstitution.subst_vars newsubst ty
+ | _ -> raise ReferenceToNonVariable
+ in
let t'' = fix_according_to_type ty t' [] in
(uri,t'')::newsubst
) [] exp_named_subst)