(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
-
val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
-val set_default_sig: unit -> unit
-val get_sig: eq_sig_type -> NCic.term
-val mk_proof:
- ?demod:bool
- -> NCic.term Terms.bag
- -> Terms.M.key
- -> NCic.term Terms.substitution
- -> Terms.M.key list
- -> NCic.term * NCic.term (* proof, type *)
+val mk_proof:NCic.term Terms.bag -> Terms.M.key -> Terms.M.key list -> NCic.term