Fixing injection bug #3616 on sigma-types.

1 files changed, 5 insertions, 2 deletions

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 *)