From 50b20a3076c5c8dfe4cf77ccfa65f33c873a2fab Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 13 Sep 2014 10:29:25 +0200
Subject: Fixing injection bug #3616 on sigma-types.

---
 tactics/equality.ml           | 7 +++++--
 test-suite/bugs/closed/3616.v | 3 +++
 2 files changed, 8 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/3616.v

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 5e94f1b3b0..4020a93fd3 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1240,11 +1240,14 @@ let inject_if_homogenous_dependent_pair ty =
     (* fetch the informations of the  pair *)
     let ceq = Universes.constr_of_global Coqlib.glob_eq in
     let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
+    let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in
     (* check whether the equality deals with dep pairs or not *)
     let eqTypeDest = fst (decompose_app t) in
     if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit;
-    let _,ar1 = decompose_app_vect t1 and
-        _,ar2 = decompose_app_vect t2 in
+    let hd1,ar1 = decompose_app_vect t1 and
+        hd2,ar2 = decompose_app_vect t2 in
+    if not (Globnames.is_global (existTconstr()) hd1) then raise Exit;
+    if not (Globnames.is_global (existTconstr()) hd2) then raise Exit;
     let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
     (* check if the user has declared the dec principle *)
     (* and compare the fst arguments of the dep pair *)
diff --git a/test-suite/bugs/closed/3616.v b/test-suite/bugs/closed/3616.v
new file mode 100644
index 0000000000..688700260c
--- /dev/null
+++ b/test-suite/bugs/closed/3616.v
@@ -0,0 +1,3 @@
+(* Was failing from April 2014 to September 2014 because of injection *)
+Goal forall P e es t, (e :: es = existT P tt t :: es)%list -> True.
+inversion 1.
-- 
cgit v1.2.3