- | Step of substitution * (rule * int * (Utils.pos * int) * Cic.term)
-
-and old_proof =
- NoProof
- | BasicProof of substitution * Cic.term
- | ProofBlock of substitution * UriManager.uri * (Cic.name * Cic.term) *
- Cic.term * (Utils.pos * equality) * old_proof
- | ProofGoalBlock of old_proof * old_proof
- | ProofSymBlock of Cic.term list * old_proof
- | 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 apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv
-val ppsubst : substitution -> string
-val buildsubst :
- int -> Cic.context -> Cic.term -> Cic.term -> substitution ->
- substitution
-val flatten_subst : substitution -> substitution
-val lookup_subst : Cic.term -> substitution -> Cic.term
-val filter : substitution -> Cic.metasenv -> Cic.metasenv
-val is_in_subst : int -> substitution -> bool
-val merge_subst_if_possible:
- substitution -> substitution ->
- substitution option
-
-val reset : unit -> unit
+ | Step of Subst.substitution * (rule * int * (Utils.pos * int) * Cic.term)
+
+and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
+
+type goal = goal_proof * Cic.metasenv * Cic.term
+
+val pp_proof:
+ equality_bag ->
+ (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int ->
+ Cic.term -> string