| SubProof of Cic.term * int * old_proof
and goal_proof = (Utils.pos * int * substitution * Cic.term) list
-
+
+val pp_proof: (Cic.name option) list -> goal_proof -> string
val empty_subst : substitution
val apply_subst : substitution -> Cic.term -> Cic.term
val string_of_proof_old : ?names:(Cic.name option)list -> old_proof -> string
val string_of_proof_new :
?names:(Cic.name option)list -> new_proof -> goal_proof -> string
-val build_proof_term_new: new_proof -> Cic.term * Cic.metasenv
+val build_proof_term_new: new_proof -> Cic.term
val build_proof_term_old: ?noproof:Cic.term -> old_proof -> Cic.term
-val build_goal_proof:
- goal_proof -> (Cic.term * Cic.metasenv) -> Cic.term * Cic.metasenv
+val build_goal_proof: goal_proof -> Cic.term -> Cic.term
val refl_proof: Cic.term -> Cic.term -> Cic.term
(** ensures that metavariables in equality are unique *)
val fix_metas: int -> equality -> int * equality