diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 7 |
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 *) |