Adapt to coq/coq#17836 (sort poly)

lukaszcz · Nov 7, 2023 · 3b59f1e · 3b59f1e
1 parent a044248
commit 3b59f1e
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/src/lib/hhutils.ml b/src/lib/hhutils.ml
@@ -296,9 +296,9 @@ let map_fold_constr f acc evd t =
        let (acc1, a') = hlp m acc a in
        let (acc2, args') = fold_arr m acc1 args in
        f m acc2 (mkApp(a',args'))
-    | Proj (p,c) ->
+    | Proj (p,r,c) ->
        let (acc1, c') = hlp m acc c in
-       f m acc1 (mkProj(p,c'))
+       f m acc1 (mkProj(p,r,c'))
     | Evar ((evk, _) as ev) ->
        let cl = Evd.expand_existential evd ev in
        let (acc1, cl') = fold_list m acc cl in
@@ -366,7 +366,7 @@ let fold_constr f acc evd t =
        let acc1 = hlp m acc a in
        let acc2 = fold_arr m acc1 args in
        f m acc2 t
-    | Proj (p,c) ->
+    | Proj (p,_,c) ->
        let acc1 = hlp m acc c in
        f m acc1 t
     | Evar ev ->
@@ -430,7 +430,7 @@ let fold_constr_shallow f acc evd t =
        let acc1 = hlp acc a in
        let acc2 = fold_arr acc1 args in
        f acc2 t
-    | Proj (p,c) ->
+    | Proj (p,_,c) ->
        let acc1 = hlp acc c in
        f acc1 t
     | Evar ev ->
@@ -500,9 +500,9 @@ let map_fold_constr_ker f acc t =
        let (acc1, a') = hlp m acc a in
        let (acc2, args') = fold_arr m acc1 args in
        f m acc2 (mkApp(a',args'))
-    | Proj (p,c) ->
+    | Proj (p,r,c) ->
        let (acc1, c') = hlp m acc c in
-       f m acc1 (mkProj(p,c'))
+       f m acc1 (mkProj(p,r,c'))
     | Evar _ -> assert false
     | Case (ci,u,pms,p,iv,c,bl) ->
        let (acc, pms') = fold_arr m acc pms in

diff --git a/src/plugin/hammer_main.ml b/src/plugin/hammer_main.ml
@@ -92,7 +92,7 @@ let rec hhterm_of (t : Constr.t) : Hh_term.hhterm =
   | App (f,args)      ->
      tuple [mk_id "$App"; hhterm_of f; hhterm_of_constrarray args]
   | Const (c,u)       -> hhterm_of_constant c
-  | Proj (p,c)        -> tuple [mk_id "$Proj";
+  | Proj (p,_,c)        -> tuple [mk_id "$Proj";
                                 hhterm_of_constant (Projection.constant p);
                                 hhterm_of_bool (Projection.unfolded p);
                                 hhterm_of c]