aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/micromega/coq_micromega.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index d4bafe773f..7adae148bd 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -846,7 +846,7 @@ struct
match env with
| [] -> ([v],n)
| e::l ->
- if EConstr.eq_constr sigma e v
+ if EConstr.eq_constr_nounivs sigma e v
then (env,n)
else
let (env,n) = _add l ( n+1) v in