From 8cbb01a852c950f044c6f2c9a9ada2626d2bbfc5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 13 Jun 2020 21:17:17 +0200
Subject: [ssr] fix env handling in error message (fix #12507)

---
 plugins/ssr/ssrequality.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index e25fc1100d..da623703a2 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -394,12 +394,16 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
     let hd_ty, miss = match EConstr.kind sigma c with
     | App (hd, args) ->
         let hd_ty = Retyping.get_type_of env sigma hd in
-        let names = let rec aux t = function 0 -> [] | n ->
+        let names = let rec aux env t = function 0 -> [] | n ->
           let t = Reductionops.whd_all env sigma t in
           let open EConstr in
           match kind_of_type sigma t with
-          | ProdType (name, _, t) -> name.binder_name :: aux t (n-1)
-          | _ -> assert false in aux hd_ty (Array.length args) in
+          | ProdType (name, ty, t) ->
+              name.binder_name ::
+                aux (EConstr.push_rel (Context.Rel.Declaration.LocalAssum (name,ty)) env) t (n-1)
+          | _ ->
+              (* In the case the head is an HO constant it may accept more arguments *)
+              CList.init n (fun _ -> Names.Name.Anonymous) in aux env hd_ty (Array.length args) in
         hd_ty, Util.List.map_filter (fun (t, name) ->
           let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in
           let open_evs = List.filter (fun k ->
-- 
cgit v1.2.3