diff options
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index 8e6b8f60c..a86b9779b 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -102,10 +102,6 @@ val eq_constr_univs_infer_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [c]. *) -val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained - (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) |