aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/coq_micromega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
-rw-r--r--plugins/micromega/coq_micromega.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index e4b58a56f..97f29df82 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -383,7 +383,6 @@ struct
let coq_and = lazy (init_constant "and")
let coq_or = lazy (init_constant "or")
let coq_not = lazy (init_constant "not")
- let coq_not_gl_ref = (Nametab.locate ( Libnames.qualid_of_string "Coq.Init.Logic.not"))
let coq_iff = lazy (init_constant "iff")
let coq_True = lazy (init_constant "True")