- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
let ty_sort1,_ =
let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
let ty_sort1,_ =
(* used only by te old auto *)
let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
(* used only by te old auto *)
let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
- let (_, metasenv, _, _) = proof in
+ let (_, metasenv, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in
let set = signature_of_hypothesis context metasenv in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in
let set = signature_of_hypothesis context metasenv in
- let (_, metasenv, _, _) = proof in
+ let (_, metasenv, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants =
match signature with
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants =
match signature with
- let (_, metasenv, _, _) = proof in
+ let (_, metasenv, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
match signature with
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
match signature with
~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
((proof, goal) as status)
=
~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
((proof, goal) as status)
=
- let (_, metasenv, _, _) = proof in
+ let (_, metasenv, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
match signature with
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
match signature with