reflexivity, symmetry, symmetry ... in e transitivity now fall-back

to their setoid_* counterparts.


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

5 files changed, 33 insertions, 9 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 97673385a8..80f7f2ef57 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1148,7 +1148,8 @@ let relation_class_that_matches_a_constr caller_name raise_opt new_goals hypt =
  let rec get_all_but_last_two =
   function
      []
-   | [_] -> assert false
+   | [_] ->
+      errorlabstrm caller_name (prterm hypt ++ str " is not a setoid equality.")
    | [_;_] -> []
    | he::tl -> he::(get_all_but_last_two tl) in
  let all_aeq_args = get_all_but_last_two hargs in
@@ -1829,3 +1830,9 @@ let setoid_transitivity c gl =
              (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
  with
   Use_transitivity -> transitivity c gl
+;;
+
+Tactics.register_setoid_reflexivity setoid_reflexivity;;
+Tactics.register_setoid_symmetry setoid_symmetry;;
+Tactics.register_setoid_symmetry_in setoid_symmetry_in;;
+Tactics.register_setoid_transitivity setoid_transitivity;;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e6b2f76ecf..ad17f52483 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1747,9 +1747,12 @@ let dImp cls =
 
 (* Reflexivity tactics *)
 
+let setoid_reflexivity = ref (fun _ -> assert false)
+let register_setoid_reflexivity f = setoid_reflexivity := f
+
 let reflexivity gl =
   match match_with_equation (pf_concl gl) with
-    | None -> error "The conclusion is not a substitutive equation" 
+    | None -> !setoid_reflexivity gl
     | Some (hdcncl,args) ->  one_constructor 1 NoBindings gl
 
 let intros_reflexivity  = (tclTHEN intros reflexivity)
@@ -1761,9 +1764,12 @@ let intros_reflexivity  = (tclTHEN intros reflexivity)
    defined and the conclusion is a=b, it solves the goal doing (Cut
    b=a;Intro H;Case H;Constructor 1) *)
 
+let setoid_symmetry = ref (fun _ -> assert false)
+let register_setoid_symmetry f = setoid_symmetry := f
+
 let symmetry gl =
   match match_with_equation (pf_concl gl) with
-    | None -> error "The conclusion is not a substitutive equation" 
+    | None -> !setoid_symmetry gl
     | Some (hdcncl,args) ->
         let hdcncls = string_of_inductive hdcncl in
         begin 
@@ -1784,12 +1790,14 @@ let symmetry gl =
 	      gl
 	end
 
+let setoid_symmetry_in = ref (fun _ _ -> assert false)
+let register_setoid_symmetry_in f = setoid_symmetry_in := f
+
 let symmetry_in id gl = 
   let ctype = pf_type_of gl (mkVar id) in 
   let sign,t = decompose_prod_assum ctype in
   match match_with_equation t with
-    | None -> (* Do not deal with setoids yet *) 
-        error "The term provided does not end with an equation" 
+    | None -> !setoid_symmetry_in id gl
     | Some (hdcncl,args) -> 
         let symccl = match args with 
 	  | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |])
@@ -1819,9 +1827,12 @@ let intros_symmetry =
    --Eduardo (19/8/97)
 *)
 
+let setoid_transitivity = ref (fun _ _ -> assert false)
+let register_setoid_transitivity f = setoid_transitivity := f
+
 let transitivity t gl =
   match match_with_equation (pf_concl gl) with
-    | None -> error "The conclusion is not a substitutive equation" 
+    | None -> !setoid_transitivity t gl
     | Some (hdcncl,args) -> 
         let hdcncls = string_of_inductive hdcncl in
         begin
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index cbc690c92c..6d0f9024b0 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -220,13 +220,17 @@ val simplest_split             : tactic
 
 (*s Logical connective tactics. *)
 
+val register_setoid_reflexivity : tactic -> unit
 val reflexivity                 : tactic
 val intros_reflexivity          : tactic
 
+val register_setoid_symmetry : tactic -> unit
 val symmetry                    : tactic
+val register_setoid_symmetry_in : (identifier -> tactic) -> unit
 val symmetry_in                 : identifier -> tactic
 val intros_symmetry             : clause -> tactic
 
+val register_setoid_transitivity : (constr -> tactic) -> unit
 val transitivity                : constr -> tactic
 val intros_transitivity         : constr -> tactic
 
diff --git a/test-suite/success/setoid_test.v8 b/test-suite/success/setoid_test.v8
index 5c62d12a14..574cb525a5 100644
--- a/test-suite/success/setoid_test.v8
+++ b/test-suite/success/setoid_test.v8
@@ -54,7 +54,7 @@ split; apply add_aux.
 assumption.
 
 rewrite H.
-setoid_reflexivity.
+reflexivity.
 Qed.
 
 Fixpoint remove (a : A) (s : set) {struct s} : set :=
diff --git a/test-suite/success/setoid_test2.v8 b/test-suite/success/setoid_test2.v8
index 72b9d03ce0..a4156c6805 100644
--- a/test-suite/success/setoid_test2.v8
+++ b/test-suite/success/setoid_test2.v8
@@ -61,6 +61,8 @@ Require Export Setoid.
 
 ### non capisce piu' le riscritture con uguaglianze quantificate (almeno
     nell'esempio di Marco)
+### Bas Spitters: poter dichiarare che ogni variabile nel contesto di tipo
+    un setoid_function e' un morfismo
 
 ### unificare le varie check_...
 ### sostituire a Use_* una sola eccezione Optimize
@@ -136,13 +138,13 @@ Add Morphism f : f_compat2. Admitted.
 Theorem test1: forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)).
  intros.
  rewrite H.
- setoid_reflexivity.
+ reflexivity.
 Qed.
 
 Theorem test1': forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)).
  intros.
  setoid_replace x with y.
- setoid_reflexivity.
+ reflexivity.
  assumption.
 Qed.