X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fsetoids.mli;h=abe71f4eb0b95326dcf2fa1145fa15c727a5d4e4;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=4c5d655cb681c42509c505a66afda47ae5673528;hpb=d7e33f1609c2d990eb52c3e30784a2aa7bdd9b32;p=helm.git

diff --git a/helm/software/components/tactics/setoids.mli b/helm/software/components/tactics/setoids.mli
index 4c5d655cb..abe71f4eb 100644
--- 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