X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicElim.mli;h=722e52f33a7884dfb2b93687579a2e729dc21772;hb=2026624f827b29c35d54aa67b301250123ea7311;hp=015b6c9d1381886fa91231ef7cc56435d40bf64d;hpb=086099d1a60948454cf0874744ef2222c2edc1b6;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli index 015b6c9d1..722e52f33 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.mli +++ b/helm/ocaml/cic_proof_checking/cicElim.mli @@ -23,18 +23,19 @@ * http://helm.cs.unibo.it/ *) -exception Failure of string + (** can't build the required elimination principle (e.g. elimination from Prop + * to Set *) +exception Can_t_eliminate + + (** internal error while generating elimination principle *) +exception Elim_failure of string (** @param sort target sort, defaults to Type * @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 +* @raise Can_t_eliminate +* @return Cic constant corresponding to the required elimination principle *) -val body_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.term +val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.obj