From eff360695af18476bfca0edfdea467cbf9203984 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 5 Dec 2019 20:57:01 +0100
Subject: Unfortunate bug with "cofix with": case of a CProdN over no bindings.

Failing on CProdN([],...) was maybe a bit too radical.
---
 plugins/ltac/g_tactic.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index d82eadcfc7..f0d6258cd1 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -135,7 +135,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
       ~hdr:"Constr:mk_cofix_tac"
       (Pp.str"Annotation forbidden in cofix expression.")) ann in
   let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
-  (id,CAst.make ~loc @@ CProdN(bl,ty))
+  (id,if bl = [] then ty else CAst.make ~loc @@ CProdN(bl,ty))
 
 (* Functions overloaded by quotifier *)
 let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
-- 
cgit v1.2.3