+type equality =
+ int * (* weight *)
+ proof * (* proof *)
+ (Cic.term * (* type *)
+ Cic.term * (* left side *)
+ Cic.term * (* right side *)
+ Utils.comparison) * (* ordering *)
+ Cic.metasenv * (* environment for metas *)
+ Cic.term list (* arguments *)
+
+and proof =
+ | NoProof
+ | BasicProof of Cic.term (* already a proof of a goal *)
+ | ProofBlock of (* proof of a rewrite step *)
+ Cic.substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
+ (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
+ | ProofGoalBlock of proof * proof
+ (* proof of the new meta, proof of the goal from which this comes *)
+ | ProofSymBlock of Cic.term list * proof (* expl.named subst, proof *)
+ | SubProof of Cic.term * int * proof
+ (* parent proof, subgoal, proof of the subgoal *)
+
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
+
+(** builds the Cic.term encoded by proof *)
+val build_proof_term: proof -> Cic.term
+
+val string_of_proof: proof -> string
+
+exception MatchingFailure
+
+(** matching between two terms. Can raise MatchingFailure *)
+val matching:
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+ CicUniv.universe_graph ->
+ Cic.substitution * Cic.metasenv * CicUniv.universe_graph