parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / setoids.mli

diff --git a/helm/software/components/tactics/setoids.mli b/helm/software/components/tactics/setoids.mli
index 4c5d655cb681c42509c505a66afda47ae5673528..abe71f4eb0b95326dcf2fa1145fa15c727a5d4e4 100644 (file)
--- a/helm/software/components/tactics/setoids.mli
+++ b/helm/software/components/tactics/setoids.mli
@@ -54,7 +54,7 @@ val general_s_rewrite : bool -> Cic.term -> new_goals:Cic.term list -> ProofEngi
 val general_s_rewrite_in :
  string -> bool -> Cic.term -> new_goals:Cic.term list -> ProofEngineTypes.tactic
 
-val setoid_reflexivity : ProofEngineTypes.tactic
+val setoid_reflexivity_tac : ProofEngineTypes.tactic
 val setoid_symmetry : ProofEngineTypes.tactic
 val setoid_symmetry_in : string -> ProofEngineTypes.tactic
 val setoid_transitivity : Cic.term -> ProofEngineTypes.tactic