Changement de comportement de rewrite: face a une egalité setoid, on

arrete de reduire brutalement pour essayer de tomber sur une egalité
Coq. Au contraire, si la relation de tete est une relation declarée 
dans la base des setoids, on l'utilise. 

ATTENTION: ceci brise la compatibilité, dans le cas très improbable 
ou quelqu'un aurait defini un setoid mais exploiterait la "feature" 
de la reduction vers l'eventuelle egalité Coq sous-jacente. 



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

2 files changed, 42 insertions, 19 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3961ab645..ddeed16d5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -69,27 +69,47 @@ let elimination_sort_of_clause = function
   | None -> elimination_sort_of_goal
   | Some id -> elimination_sort_of_hyp id
 
+(* The next function decides in particular whether to try a regular 
+  rewrite or a setoid rewrite. 
+
+  Old approach was: 
+   break everything, if [eq] appears in head position 
+   then regular rewrite else try setoid rewrite
+ 
+  New approach is: 
+   if head position is a known setoid relation then setoid rewrite
+   else back to the old approach
+*)
+
 let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
   let ctype = pf_type_of gl c in 
-  let env = pf_env gl in
-  let sigma = project gl in 
-  let _,t = splay_prod env sigma ctype in
-  match match_with_equation t with
-    | None -> 
-	if l = NoBindings
-	then general_s_rewrite_clause cls lft2rgt c [] gl
-	else error "The term provided does not end with an equation" 
-    | Some (hdcncl,_) -> 
-        let hdcncls = string_of_inductive hdcncl in 
-	let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
-        let dir = if cls=None then lft2rgt else not lft2rgt in
-        let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
-        let elim =
-	  try pf_global gl (id_of_string rwr_thm)
-          with Not_found ->
-            error ("Cannot find rewrite principle "^rwr_thm)
-        in 
-	general_elim_clause cls (c,l) (elim,NoBindings) gl
+  (* A delta-reduction would be here too strong, since it would 
+     break search for a defined setoid relation in head position. *)
+  let t = snd (decompose_prod (whd_betaiotazeta ctype)) in 
+  let head = if isApp t then fst (destApp t) else t in 
+  if relation_table_mem head && l = NoBindings then 
+    general_s_rewrite_clause cls lft2rgt c [] gl
+  else 
+    (* Original code. In particular, [splay_prod] performs delta-reduction. *)
+    let env = pf_env gl in
+    let sigma = project gl in 
+    let _,t = splay_prod env sigma t in
+    match match_with_equation t with
+      | None -> 
+	  if l = NoBindings
+	  then general_s_rewrite_clause cls lft2rgt c [] gl
+	  else error "The term provided does not end with an equation" 
+      | Some (hdcncl,_) -> 
+          let hdcncls = string_of_inductive hdcncl in 
+	  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+          let dir = if cls=None then lft2rgt else not lft2rgt in
+          let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
+          let elim =
+	    try pf_global gl (id_of_string rwr_thm)
+            with Not_found ->
+              error ("Cannot find rewrite principle "^rwr_thm)
+          in 
+	  general_elim_clause cls (c,l) (elim,NoBindings) gl
 
 let general_rewrite_bindings = general_rewrite_bindings_clause None
 let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings)
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 09fb39da8..b8bed63c5 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -75,3 +75,6 @@ val add_setoid :
 
 val new_named_morphism :
  Names.identifier -> constr_expr -> morphism_signature option -> unit
+
+val relation_table_find : constr -> relation
+val relation_table_mem : constr -> bool