aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eqdecide.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/eqdecide.mli')
-rw-r--r--tactics/eqdecide.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eqdecide.mli b/tactics/eqdecide.mli
index cb48a5bcc..dca1780b7 100644
--- a/tactics/eqdecide.mli
+++ b/tactics/eqdecide.mli
@@ -14,4 +14,4 @@
val decideEqualityGoal : unit Proofview.tactic
-val compare : Constr.t -> Constr.t -> unit Proofview.tactic
+val compare : EConstr.t -> EConstr.t -> unit Proofview.tactic