*)
exception Impossible of int
-exception ReferenceToDefinition
-exception ReferenceToAxiom
+exception ReferenceToConstant
exception ReferenceToVariable
exception ReferenceToCurrentProof
exception ReferenceToInductiveDefinition
exception WrongShape
exception AlreadySimplified
-val syntactic_equality : Cic.term -> Cic.term -> bool
+val alpha_equivalence: Cic.term -> Cic.term -> bool
val replace :
equality:(Cic.term -> 'a -> bool) ->
what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
-val reduce :
- (Cic.name * Cic.context_entry) option list -> Cic.term -> Cic.term
+val replace_lifting :
+ equality:(Cic.term -> Cic.term -> bool) ->
+ what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term
+val reduce : Cic.context -> Cic.term -> Cic.term
val simpl : Cic.context -> Cic.term -> Cic.term