diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-23 12:37:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-08 20:46:08 +0200 |
| commit | a9f8fa56e76aa557b1391cb9709cb893a4f602ce (patch) | |
| tree | 9ef357486083ebefa0a9b2ef328270b74f5dad93 /engine/universes.mli | |
| parent | b1fbec7e3945fe2965f4ba9f80c8c31b821dbce1 (diff) | |
Using EConstr equality check in unification.
The code from Universes what essentially a duplicate of the one from EConstr,
but they were copied for historical reasons. Now, this is not useful anymore,
so that we remove the implementation from Universes and rely on the one from
EConstr.
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index fe40f8238..8b2217d44 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -67,11 +67,6 @@ val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_f val to_constraints : UGraph.t -> universe_constraints -> constraints -(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, - application grouping, the universe constraints in [u] and additional constraints [c]. *) -val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> - constr -> constr -> 'a -> 'a option - (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) @@ -80,20 +75,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 -(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] - modulo alpha, casts, application grouping, the universe constraints - in [u] and additional constraints [c]. *) -val leq_constr_univs_infer : 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 : constr -> constr -> universe_constraints option - -(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe constraints in [c]. *) -val leq_constr_universes : constr -> constr -> universe_constraints 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 |