package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val goal_equal : evd:Evd.evar_map -> extended_evd:Evd.evar_map -> Evar.t -> Evar.t -> bool

goal_equal ~evd ~extended_evd evar extended_evar tests whether the evar_info from evd corresponding to evar is equal to that from extended_evd corresponding to extended_evar, up to existential variable instantiation and equalisable universes. The universe constraints in extended_evd are assumed to be an extension of the universe constraints in evd.

OCaml

Innovation. Community. Security.