diff options
| -rw-r--r-- | tactics/equality.ml | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3616.v | 3 |
2 files changed, 8 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 *) 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. |