From 4da7ddb8c3c2f1dafd5d9187741659a9332b75c2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 21 Mar 2013 19:50:03 +0000
Subject: Firstorder: record with defined field aren't conjonctions (fix #2629)

 The let-in in the type of constructor was perturbating the
 Hipattern.dependent check, leading firstorder to consider too much
 inductives as dependent-free conjonctions, ending with lift errors
 (UNBOUND_REL_-2, ouch).

 This patch is probably overly cautious : if the variable of the
 let-in is used, we consider the constructor to be dependent.
 If someday somebody feels it necessary, he/she could try to reduce
 the let-in's instead...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16339 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/hipattern.ml4 | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 286aa94929..ede813cdba 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -58,9 +58,12 @@ let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
 
 (* Test dependencies *)
 
+(* NB: we consider also the let-in case in the following function,
+   since they may appear in types of inductive constructors (see #2629) *)
+
 let rec has_nodep_prod_after n c =
   match kind_of_term c with
-    | Prod (_,_,b) ->
+    | Prod (_,_,b) | LetIn (_,_,_,b) ->
 	( n>0 || not (dependent (mkRel 1) b))
 	&& (has_nodep_prod_after (n-1) b)
     | _            -> true
-- 
cgit v1.2.3