diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-04 18:58:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:05:31 +0100 |
| commit | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (patch) | |
| tree | fceac407f6e4254e107817b6140257bcc8f9755a /kernel/constr.ml | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
[api] Deprecate all legacy uses of Names in core.
This will allow to merge back `Names` with `API.Names`
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index c3e609536..cec00c04b 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -75,7 +75,7 @@ type ('constr, 'types) pfixpoint = type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration type 'a puniverses = 'a Univ.puniverses -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses @@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of (constant * 'univs) + | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array @@ -520,7 +520,7 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = eq c1 c2 && Array.equal_norefl eq l1 l2 | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2 - | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2 + | Const (c1,u1), Const (c2,u2) -> Constant.equal c1 c2 && eq_universes true u1 u2 | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2 | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> @@ -681,7 +681,7 @@ let constr_ord_int f t1 t2 = | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> (Evar.compare =? (Array.compare f)) e1 e2 l1 l2 - | Const (c1,u1), Const (c2,u2) -> con_ord c1 c2 + | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2 | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2 | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> |