Proposition de correction pour le bug #1173 (ou du moins pour un

exemple de divergence soumis par Andrew Appel) [on renonce à
normaliser pour trouver l'ensemble minimal de variables liées dans le
2e membre d'une égalité dépendante]



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9765 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 7 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f00cdcd00d..ee950e55ff 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -578,18 +578,20 @@ let make_tuple env sigma (rterm,rty) lind =
    applist(sig_term,[a;p]))
 
 (* check that the free-references of the type of [c] are contained in
-   the free-references of the normal-form of that type.  If the normal
-   form of the type contains fewer references, we want to return that
-   instead. *)
+   the free-references of the normal-form of that type. Strictly
+   computing the exact set of free rels would require full
+   normalization but this is not reasonable (e.g. in presence of
+   records that contains proofs). We restrict ourself to a "simpl"
+   normalization *)
 
 let minimal_free_rels env sigma (c,cty) =
   let cty_rels = free_rels cty in
-  let nf_cty = nf_betadeltaiota env sigma cty in
-  let nf_rels = free_rels nf_cty in
-  if Intset.subset cty_rels nf_rels then
+  let cty' = simpl env sigma cty in
+  let rels' = free_rels cty' in
+  if Intset.subset cty_rels rels' then
     (cty,cty_rels)
   else
-    (nf_cty,nf_rels)
+    (cty',rels')
 
 (* [sig_clausal_form siglen ty]