+
+ let indent = ref 0 in
+
+ let rec do_build_proof proof =
+ match proof with
+ | NoProof ->
+ Printf.fprintf stderr "WARNING: no proof!\n";
+(* (string_of_equality equality); *)
+ Cic.Implicit None
+ | BasicProof term -> term
+ | ProofGoalBlock (proofbit, proof (* equality *)) ->
+ print_endline "found ProofGoalBlock, going up...";
+(* let _, proof, _, _, _ = equality in *)
+ do_build_goal_proof proofbit proof
+ | ProofSymBlock (ens, proof) ->
+ let proof = do_build_proof proof in
+ Cic.Appl [
+ Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
+ proof
+ ]
+ | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) ->
+(* Printf.printf "\nsubst:\n%s\n" (print_subst subst); *)
+(* print_newline (); *)
+
+(* let name, ty, eq_ty, left, right = t' in *)
+(* let bo = *)
+(* Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); *)
+(* eq_ty; left; right] *)
+(* in *)
+ let t' = Cic.Lambda (name, ty, bo) in
+ (* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
+ (* (string_of_equality eq) (string_of_equality eq'); *)
+ (* print_newline (); *)
+
+(* let s = String.make !indent ' ' in *)
+(* incr indent; *)
+
+(* print_endline (s ^ "build proof'------------"); *)
+
+ let proof' =
+ let _, proof', _, _, _ = eq in
+ do_build_proof proof'
+ in
+(* print_endline (s ^ "END proof'"); *)
+
+(* print_endline (s ^ "build eqproof-----------"); *)
+
+ let eqproof = do_build_proof eqproof in
+
+(* print_endline (s ^ "END eqproof"); *)
+(* decr indent; *)
+
+
+ let _, _, (ty, what, other, _), menv', args' = eq in
+ let what, other =
+ if pos = Utils.Left then what, other else other, what
+ in
+ CicMetaSubst.apply_subst subst
+ (Cic.Appl [Cic.Const (eq_URI, []); ty;
+ what; t'; eqproof; other; proof'])
+
+ and do_build_goal_proof proofbit proof =
+(* match proofbit with *)
+(* | BasicProof _ -> do_build_proof proof *)
+(* | proofbit -> *)
+ match proof with
+ | ProofGoalBlock (pb, p(* eq *)) ->
+ do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p(* eq *)))
+(* let _, proof, _, _, _ = eq in *)
+(* let newproof = replace_proof proofbit proof in *)
+(* do_build_proof newproof *)
+
+(* | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *)
+(* let eqproof' = replace_proof proofbit eqproof in *)
+(* do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *)
+ | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
+
+ and replace_proof newproof = function
+ | ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof) ->
+ let eqproof' = replace_proof newproof eqproof in
+ ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof')
+ | ProofGoalBlock (pb, p(* equality *)) ->
+ let pb' = replace_proof newproof pb in
+ ProofGoalBlock (pb', p(* equality *))
+(* let w, proof, t, menv, args = equality in *)
+(* let proof' = replace_proof newproof proof in *)
+(* ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
+ | BasicProof _ -> newproof
+ | p -> p
+ in