diff options
Diffstat (limited to 'tactics/eqdecide.ml')
| -rw-r--r-- | tactics/eqdecide.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 7909b669b..c18fd31d0 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -82,8 +82,6 @@ let solveNoteqBranch side = let make_eq () = (*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) -let make_eq_refl () = -(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ()) let mkDecideEqGoal eqonleft op rectype c1 c2 = let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in |