From 13e4331494ea5bd2b37cb5730ac15662a9067772 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Aug 2020 20:14:47 +0200
Subject: Quick fix to #12787 (injection anomaly due to inconsistent comp. of
 free vars).

We fix it by reducing K-redexes the same in the both places
(make_tuple and minimal_free_rels) which compute the dependencies of a
dependent equality.
---
 tactics/equality.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f1326a51a9..b4def7bb51 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1134,6 +1134,7 @@ let make_tuple env sigma (rterm,rty) lind =
   assert (not (noccurn sigma lind rty));
   let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
   let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
+  let a = simpl env sigma a in
   let na = Context.Rel.Declaration.get_annot (lookup_rel lind env) in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
-- 
cgit v1.2.3