Integer-indexed types

src/ecAlgTactic.ml

@@ -80,7 +80,7 @@ module Axioms = struct
     let addctt = fun subst x f -> EcSubst.add_opdef subst (xpath x) ([], f) in
 
     let subst  =
-      EcSubst.add_tydef EcSubst.empty (xpath tname) ([], cr.r_type) in
+      EcSubst.add_tydef EcSubst.empty (xpath tname) ([], [], cr.r_type) in
     let subst  =
       List.fold_left (fun subst (x, p) -> add subst x p) subst crcore in
     let subst  = odfl subst (cr.r_opp |> omap (fun p -> add subst opp p)) in
@@ -123,7 +123,7 @@ module Axioms = struct
 
     let for1 axname =
       let ax = EcEnv.Ax.by_path (EcPath.pqname tmod axname) env in
-        assert (ax.ax_tparams = [] && is_axiom ax.ax_kind);
+        assert (ax.ax_tparams.tyvars = [] && ax.ax_tparams.idxvars = [] && is_axiom ax.ax_kind);
         (axname, EcSubst.subst_form subst ax.ax_spec)
     in
       List.map for1 axs

src/ecAlgebra.ml

@@ -75,7 +75,7 @@ type eq = form * form
 (* -------------------------------------------------------------------- *)
 let rapp r op args =
   let opty = toarrow (List.map f_ty args) r.r_type in
-    f_app (f_op op [] opty) args r.r_type
+    f_app (f_op op opty) args r.r_type
 
 let rzero r = rapp r r.r_zero []
 let rone  r = rapp r r.r_one  []

src/ecAlphaInvHashtbl.ml

@@ -78,7 +78,7 @@ let hash_memo (memo : (int, int) Hashtbl.t) (f0 : form) : int =
       combine 3 (pv_hash pv)
     | Fglob (mp, _m) -> combine 4 (id_hash mp)
     | Fop (p, tys) ->
-      combine 5 (combine_list (EcPath.p_hash p) (List.map ty_hash tys))
+      combine 5 (combine_list (EcPath.p_hash p) (List.map ty_hash tys.types))
     | Fif (c, t, f) -> combine 6 (combine_list 0 [hash e c; hash e t; hash e f])
     | Fmatch (c, bs, ty) ->
       combine 7 (combine_list (ty_hash ty) (hash e c :: List.map (hash e) bs))