-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 (* no proof *)
- | 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: ?noproof:Cic.term -> proof -> Cic.term
-
-val string_of_proof: proof -> string
-