diff options
Diffstat (limited to 'library/assumptions.ml')
| -rw-r--r-- | library/assumptions.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml index cb0c99e5a..ee916c237 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -22,8 +22,6 @@ open Term open Declarations open Mod_subst -let cst_ord k1 k2 = kn_ord (canonical_con k1) (canonical_con k2) - type context_object = | Variable of Id.t (* A section variable or a Let definition *) | Axiom of constant (* An axiom or a constant. *) @@ -37,9 +35,9 @@ struct let compare x y = match x , y with | Variable i1 , Variable i2 -> Id.compare i1 i2 - | Axiom k1 , Axiom k2 -> cst_ord k1 k2 - | Opaque k1 , Opaque k2 -> cst_ord k1 k2 - | Transparent k1 , Transparent k2 -> cst_ord k1 k2 + | Axiom k1 , Axiom k2 -> con_ord k1 k2 + | Opaque k1 , Opaque k2 -> con_ord k1 k2 + | Transparent k1 , Transparent k2 -> con_ord k1 k2 | Axiom _ , Variable _ -> 1 | Opaque _ , Variable _ | Opaque _ , Axiom _ -> 1 |