helm/interface/cicReduction.mli

   1 exception WrongUriToInductiveDefinition
   2 exception ReferenceToDefinition
   3 exception ReferenceToAxiom
   4 exception ReferenceToVariable
   5 exception ReferenceToCurrentProof
   6 exception ReferenceToInductiveDefinition
   7 val fdebug : int ref
   8 val whd : Cic.term -> Cic.term
   9 val are_convertible : Cic.term -> Cic.term -> bool