diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ceb651abed..8ca7b48a32 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -745,7 +745,7 @@ struct (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *) let eq_constr gl x y = let evd = gl.sigma in - match EConstr.eq_constr_universes gl.env evd x y with + match EConstr.eq_constr_universes_proj gl.env evd x y with | Some csts -> let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in begin @@ -769,15 +769,16 @@ struct ({vars=vars';gl=gl'}, CamlToCoq.positive n) let get_rank env v = - let evd = env.gl.sigma in + let gl = env.gl in let rec _get_rank env n = match env with | [] -> raise (Invalid_argument "get_rank") | e::l -> - if EConstr.eq_constr evd e v - then n - else _get_rank l (n+1) in + match eq_constr gl e v with + | Some _ -> n + | None -> _get_rank l (n+1) + in _get_rank env.vars 1 let elements env = env.vars |