Protection erreur find_eq_data dans decompEqThen et uniformisation messages d'erreur, et généralisation onNegatedEquality

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

1 files changed, 30 insertions, 36 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index fc2ce75f23..a7e8c356e5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -18,6 +18,7 @@ open Termops
 open Inductive
 open Inductiveops
 open Environ
+open Libnames
 open Reductionops
 open Instantiate
 open Typeops
@@ -419,14 +420,8 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
 
 exception NotDiscriminable
 
-let discr id gls =
-  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
+let discrEq (lbeq,(t,t1,t2)) id gls =
   let sort = pf_type_of gls (pf_concl gls) in 
-  let (lbeq,(t,t1,t2)) =
-    try find_eq_data_decompose eqn
-    with PatternMatchingFailure ->
-      errorlabstrm "discr" (pr_id id ++ str": not a primitive equality here")
-  in
   let sigma = project gls in
   let env = pf_env gls in
   (match find_positions env sigma t1 t2 with
@@ -445,24 +440,34 @@ let discr id gls =
 			([onLastHyp gen_absurdity;
 			  refine (mkApp (pf, [| mkVar id |]))]))) gls)
 
-
 let not_found_message id =
   (str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++
     str" was not found in the current environment")
 
-let onNegatedEquality tac gls =
-  if is_matching_not (pf_concl gls) then
-    (tclTHEN (tclTHEN hnf_in_concl intro) (onLastHyp tac)) gls
-  else if is_matching_imp_False (pf_concl gls)then
-    (tclTHEN intro (onLastHyp tac)) gls
-  else 
-    errorlabstrm "extract_negated_equality_then"
-      (str"The goal should negate an equality")
+let onEquality tac id gls =
+  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
+  let eq =
+    try find_eq_data_decompose eqn
+    with PatternMatchingFailure ->
+      errorlabstrm "" (pr_id id ++ str": not a primitive equality") 
+  in tac eq id gls
 
+let onNegatedEquality tac gls =
+  let ccl = pf_concl gls in
+  let eq =
+    try match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with
+      | Prod (_,t,u) when is_empty_type u ->
+          find_eq_data_decompose (pf_whd_betadeltaiota gls t)
+      | _ -> raise PatternMatchingFailure
+    with PatternMatchingFailure ->
+      errorlabstrm "" (str "Not a negated primitive equality")
+  in tclTHEN introf (onLastHyp (tac eq)) gls
 
 let discrSimpleClause = function
-  | None -> onNegatedEquality discr
-  | Some (id,_,_) -> discr id
+  | None -> onNegatedEquality discrEq
+  | Some (id,_,_) -> onEquality discrEq id
+
+let discr = onEquality discrEq
 
 let discrClause = onClauses discrSimpleClause
 
@@ -695,13 +700,7 @@ let try_delta_expand env sigma t =
    expands then only when the whdnf has a constructor of an inductive type
    in hd position, otherwise delta expansion is not done *)
 
-let inj id gls =
-  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
-  let (eq,(t,t1,t2))= 
-    try find_eq_data_decompose eqn
-    with PatternMatchingFailure ->
-      errorlabstrm "Inj" (pr_id id ++ str": not a primitive equality here") 
-  in
+let injEq (eq,(t,t1,t2)) id gls =
   let sigma = project gls in
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
@@ -749,17 +748,17 @@ let inj id gls =
 	     in ((tclTHENS  (cut  ty) ([tclIDTAC;refine pf]))))
 	  injectors
 	  gls
-	    
+
+let inj = onEquality injEq
+
 let injClause = function
-  | None -> onNegatedEquality inj
+  | None -> onNegatedEquality injEq
   | Some id -> try_intros_until inj id
 
 let injConcl gls  = injClause None gls
 let injHyp id gls = injClause (Some id) gls
 
-let decompEqThen ntac id gls =
-  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
-  let (lbeq,(t,t1,t2))= find_eq_data_decompose eqn in
+let decompEqThen ntac (lbeq,(t,t1,t2)) id gls =
   let sort = pf_type_of gls (pf_concl gls) in 
   let sigma = project gls in
   let env = pf_env gls in 
@@ -806,17 +805,12 @@ let decompEqThen ntac id gls =
 	      (ntac (List.length injectors)))
 	  gls))
 
-let decompEq = decompEqThen (fun x -> tclIDTAC)
-
 let dEqThen ntac = function
   | None -> onNegatedEquality (decompEqThen ntac)
-  | Some id -> try_intros_until (decompEqThen ntac) id
+  | Some id -> try_intros_until (onEquality (decompEqThen ntac)) id
 
 let dEq = dEqThen (fun x -> tclIDTAC)
 
-let dEqConcl gls = dEq None gls
-let dEqHyp id gls = dEq (Some id) gls
-
 let rewrite_msg = function 
   | None -> str "passed term is not a primitive equality" 
   | Some id -> pr_id id ++ str "does not satisfy preconditions "