diff options
| author | Gaëtan Gilbert | 2019-03-20 14:19:54 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-20 14:19:54 +0100 |
| commit | ba33839754bb6ac0f85070e95466a2b8030fdc1b (patch) | |
| tree | b0cf9609b4ed10b4acf4474edf0ef471d9e681b7 /kernel | |
| parent | b899b102e071ba0faa07949b2ee66bbb7dade23b (diff) | |
| parent | 636857d2e77ee26b4b193f3bbefee253c07dfbff (diff) | |
Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on applications
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 11958c9108..d74c96af84 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -860,7 +860,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | App (c1, l1), App (c2, l2) -> let len = Array.length l1 in Int.equal len (Array.length l2) && - eq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 + leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> |