snapshot (1st commit of fix body generation)

[helm.git] / helm / ocaml / cic_proof_checking / cicElim.mli

diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli
index b341d36a4cbe9b7a3a93d184754ebd32b18f36ea..015b6c9d1381886fa91231ef7cc56435d40bf64d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicElim.mli
+++ b/helm/ocaml/cic_proof_checking/cicElim.mli
@@ -29,6 +29,12 @@ exception Failure of string
 * @param uri inductive type uri
 * @param typeno inductive type number
 * @raise Failure
+* @return type of elimination principle for the given inductive type
 *)
 val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.term
 
+(** parameters as above
+* @return body of elimination principle for the given inductive type
+*)
+val body_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.term
+