(uri,Cic.Meta(newmeta+2,irl))::l in
aux newmeta uris
-let mk_implicit' metasenv context =
- let (metasenv, index) = mk_implicit metasenv context in
- (metasenv, index - 1, index)
-
let mk_implicit_type metasenv context =
let newmeta = new_meta metasenv in
let irl = identity_relocation_list_for_metavariable context in
let metasenv', l' = do_local_context metasenv context l in
metasenv', Cic.Meta (n, l')
| Cic.Implicit ->
- let (metasenv', type_index, _) = mk_implicit' metasenv context in
+ let (metasenv', idx) = mk_implicit metasenv context in
let irl = identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (type_index, irl)
+ metasenv', Cic.Meta (idx, irl)
| Cic.Cast (te, ty) ->
let metasenv', ty' = aux metasenv context ty in
let metasenv'', te' = aux metasenv' context te in
List.fold_right
(fun (name, _, typ, _) (metasenv, types) ->
let new_metasenv, new_type = aux metasenv context typ in
+prerr_endline ("UH? " ^ CicPp.ppterm typ ^ " ==> " ^ CicPp.ppterm new_type) ;
(new_metasenv, (name, new_type) :: types))
funs (metasenv, [])
in