-let build_segments ~terms ~proof =
- let r = mkConst r_uri proof in (* cic objects *)
- let rplus = mkConst rplus_uri proof in
- let rmult = mkConst rmult_uri proof in
- let ropp = mkConst ropp_uri proof in
- let r0 = mkConst r0_uri proof in
- let r1 = mkConst r1_uri proof in
- let interp_ap = mkConst interp_ap_uri proof in
- let interp_sacs = mkConst interp_sacs_uri proof in
- let apolynomial_normalize = mkConst apolynomial_normalize_uri proof in
- let apolynomial_normalize_ok = mkConst apolynomial_normalize_ok_uri proof in
- let rtheory = mkConst rtheory_uri proof in
+let build_segments ~terms =
+ let r = mkConst r_uri [] in (* cic objects *)
+ let rplus = mkConst rplus_uri [] in
+ let rmult = mkConst rmult_uri [] in
+ let ropp = mkConst ropp_uri [] in
+ let r1 = mkConst r1_uri [] in
+ let r0 = mkConst r0_uri [] in
+ let theory_args_subst varmap =
+ [abstract_rings_A_uri, r ;
+ abstract_rings_Aplus_uri, rplus ;
+ abstract_rings_Amult_uri, rmult ;
+ abstract_rings_Aone_uri, r1 ;
+ abstract_rings_Azero_uri, r0 ;
+ abstract_rings_Aopp_uri, ropp ;
+ abstract_rings_vm_uri, varmap] in
+ let theory_args_subst' eq varmap t =
+ [abstract_rings_A_uri, r ;
+ abstract_rings_Aplus_uri, rplus ;
+ abstract_rings_Amult_uri, rmult ;
+ abstract_rings_Aone_uri, r1 ;
+ abstract_rings_Azero_uri, r0 ;
+ abstract_rings_Aopp_uri, ropp ;
+ abstract_rings_Aeq_uri, eq ;
+ abstract_rings_vm_uri, varmap ;
+ abstract_rings_T_uri, t] in
+ let interp_ap varmap =
+ mkConst interp_ap_uri (theory_args_subst varmap) in
+ let interp_sacs varmap =
+ mkConst interp_sacs_uri (theory_args_subst varmap) in
+ let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in
+ let apolynomial_normalize_ok eq varmap t =
+ mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in
+ let rtheory = mkConst rtheory_uri [] in