let metasenv,s = aux metasenv n s in
let metasenv,t = aux metasenv (n+1) t in
metasenv,Cic.LetIn(name,s,t)
+ | Cic.Const(uri,ens) ->
+ let metasenv,ens =
+ List.fold_right
+ (fun (v,a) (metasenv,ens) ->
+ let metasenv,a' = aux metasenv n a in
+ metasenv,(v,a')::ens)
+ ens (metasenv,[])
+ in
+ metasenv,Cic.Const(uri,ens)
| t -> metasenv,t
in
aux metasenv 0 p
let passive_l = fst passive in
let ma = max_l active_l in
let mp = max_l passive_l in
- assert (maxm > max ma mp);
match LibraryObjects.eq_URI () with
| None -> active, passive, !maxmeta
| Some eq_uri ->
let passive_l = fst passive in
let ma = max_l active_l in
let mp = max_l passive_l in
- assert (maxm > max ma mp);
let proof, goalno = status in
let uri, metasenv, meta_proof, term_to_prove = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in