Big change: Qed saves the theorem/definition and registers it to the getter.

[helm.git] / helm / gTopLevel / proofEngineReduction.mli

diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli
index aa0a3a6489394056178b20314c04162bc816efbe..f185dd6638d9a3eaf30bf078039d1cadbf40d207 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.mli
+++ b/helm/gTopLevel/proofEngineReduction.mli
@@ -24,8 +24,7 @@
  *)
 
 exception Impossible of int
-exception ReferenceToDefinition
-exception ReferenceToAxiom
+exception ReferenceToConstant
 exception ReferenceToVariable
 exception ReferenceToCurrentProof
 exception ReferenceToInductiveDefinition
@@ -34,7 +33,7 @@ exception RelToHiddenHypothesis
 exception WrongShape
 exception AlreadySimplified
 
-val syntactic_equality : alpha_equivalence:bool -> 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