From 7b724139a09c5d875131c5861a32d225d5b4b07b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Feb 2019 15:52:30 +0100
Subject: Constructor type information uses the expanded form.

It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.

Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
---
 plugins/firstorder/formula.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index a60a966cec..56b3dc97cf 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -13,7 +13,6 @@ open Names
 open Constr
 open EConstr
 open Vars
-open Termops
 open Util
 open Declarations
 open Globnames
@@ -100,9 +99,8 @@ let kind_of_formula env sigma term =
 		      else
 			let has_realargs=(n>0) in
 			let is_trivial=
-			  let is_constant c =
-			    Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
-			    Array.exists is_constant mip.mind_nf_lc in
+                          let is_constant n = Int.equal n 0 in
+                            Array.exists is_constant mip.mind_consnrealargs in
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
 			  then
-- 
cgit v1.2.3