summaryrefslogtreecommitdiff
path: root/compiler/Pure.ml
diff options
context:
space:
mode:
authorSon HO2024-03-17 05:10:36 +0100
committerGitHub2024-03-17 05:10:36 +0100
commitd56946242859e0d375c1d44585b9da6d5fbe94cb (patch)
tree4589586257210809913e225192a15464cb91851f /compiler/Pure.ml
parentc33a9807cf6aa21b2364449ee756ebf93de19eca (diff)
parentee3e26e7b639bc7282d0c3777f9460e975ef232f (diff)
Merge pull request #91 from AeneasVerif/son/hax
Prepare the merge in hax
Diffstat (limited to '')
-rw-r--r--compiler/Pure.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 33c23cc3..a735667e 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -283,7 +283,7 @@ type ty =
| TVar of type_var_id
| TLiteral of literal_type
| TArrow of ty * ty
- | TTraitType of trait_ref * generic_args * string
+ | TTraitType of trait_ref * string
(** The string is for the name of the associated type *)
and trait_ref = {
@@ -374,7 +374,6 @@ type generic_params = {
type trait_type_constraint = {
trait_ref : trait_ref;
- generics : generic_args;
type_name : trait_item_name;
ty : ty;
}
@@ -599,8 +598,7 @@ type qualif_id =
| Global of global_decl_id
| AdtCons of adt_cons_id (** A function or ADT constructor identifier *)
| Proj of projection (** Field projector *)
- | TraitConst of trait_ref * generic_args * string
- (** A trait associated constant *)
+ | TraitConst of trait_ref * string (** A trait associated constant *)
[@@deriving show]
(** An instantiated qualifier.