diff options
| author | William Lawvere | 2017-06-13 22:22:36 -0700 |
|---|---|---|
| committer | William Lawvere | 2017-06-13 22:22:36 -0700 |
| commit | af39f62ad21f71a860e287e4d217b24dc9e2106b (patch) | |
| tree | 43c14ae184f24fffaf495dade6d27a1c2fac3e1a /kernel/term.ml | |
| parent | 3b0830ce0233db5b612e0b5bb92e89fa644eb0e4 (diff) | |
| parent | 7e63c300a3aa1e3befb29bab9094e8b1939824bb (diff) | |
Merge remote-tracking branch 'upstream/trunk' into trunk
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 07a85329ef..b90718358e 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -143,7 +143,8 @@ let leq_constr_univs = Constr.leq_constr_univs let eq_constr_nounivs = Constr.eq_constr_nounivs let kind_of_term = Constr.kind -let constr_ord = Constr.compare +let compare = Constr.compare +let constr_ord = compare let fold_constr = Constr.fold let map_puniverses = Constr.map_puniverses let map_constr = Constr.map |