Fixed subst failing when a truly heterogeneous JMeq hyp is in the

context (problem introduced in r12259) + improved backward
compatibility in hippatern.mli (wrt r12259).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12260 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 26 insertions, 2 deletions

diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 0b81a492a..bf34a5598 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -208,7 +208,8 @@ let match_with_unit_or_eq_type t =
 let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t)
 
 (* A unit type is an inductive type with no indices but possibly
-   (useless) parameters, and that has no constructors *)
+   (useless) parameters, and that has no arguments in its unique
+   constructor *)
 
 let is_unit_type t =
   match match_with_conjunction t with
@@ -372,9 +373,32 @@ let equalities =
    coq_jmeq_pattern, build_coq_jmeq_data;
    coq_identity_pattern, build_coq_identity_data]
 
-let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *)
+let find_eq_data eqn = (* fails with PatternMatchingFailure *)
   first_match (match_eq eqn) equalities
 
+let extract_eq_args gl = function
+  | MonomorphicLeibnizEq (e1,e2) -> 
+      let t = Tacmach.pf_type_of gl e1 in (t,e1,e2)
+  | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
+  | HeterogenousEq (t1,e1,t2,e2) ->
+      if Tacmach.pf_conv_x gl t1 t2 then (t1,e1,e2)
+      else raise PatternMatchingFailure
+
+let find_eq_data_decompose gl eqn =
+  let (lbeq,eq_args) = find_eq_data eqn in
+  (lbeq,extract_eq_args gl eq_args)
+
+let find_this_eq_data_decompose gl eqn =
+  let (lbeq,eq_args) = 
+    try find_eq_data eqn
+    with PatternMatchingFailure ->
+      errorlabstrm "" (str "No primitive equality found.") in
+  let eq_args =
+    try extract_eq_args gl eq_args
+    with PatternMatchingFailure -> 
+      error "Don't know what to do with JMeq on arguments not of same type." in
+  (lbeq,eq_args)
+
 open Tacmach
 open Tacticals