Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:

1. setoid and morphisms declaration were used to become in scope only
   when a module is imported (and to disappear when a module is closed).
   Thus it was possible to declare a setoid in a module A; a morphism on
   it in a module B that imports A; and to write a module C that imports
   B (but not A) that uses the morphism. Since the morphism is in scope
   but the setoid isn't this was a source of bugs.
   Fixed by making the setoid/morphisms declaration always in scope
   (i.e. they become in scope when the module is loaded, not when it is
   imported).
2. since it is possible to define different setoids for the same type
   / different morphisms on the same function  in separate modules and
   since it is possible to import them at once, we must allow the possibility
   to have more than one setoid for each type and more than one morphism
   for each function. The data structures of the tactic has been completely
   revised to allow this possibility. Right now warnings are used to
   highlight situations when an ambiguity is arised. In the near future
   syntax will be added to disambiguate the situation, and smart algorithms
   to find the right interpretations when more than one applies but only
   a few are succesfull. For the moment the choice of the interpretation
   (i.e. the association of a morphism to each function in the goal)
   is already done before the actual start of the tactic (in order to
   allow a modular implementation of the choice of the interpretation).
3. the tactic used to work only in those situations where all the functions
   involved in the path(s) root of the term - term(s) to replace were
   morphisms. In the case where they are simple functions (i.e. the
   ``default setoid'' is Leibniz) the tactic failed. These cases are now
   considered by making the setoid_replace tactic perform simple replace steps
   where needed. A future optimization will allow to minimize the number
   of replace steps.

The tactic should be 100% compatible with the old tactic, but for the
situations that used to fail and are now succesfull.
The declaration of setoids/morphisms can now also be succesfull where it
used to fail.


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

1 files changed, 6 insertions, 1 deletions

diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 059a25010f..02046c55b3 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -12,9 +12,14 @@ open Term
 open Proof_type
 open Topconstr
 
+
+val register_replace : (constr -> constr -> tactic) -> unit
+
+val print_setoids : unit -> unit
+
 val equiv_list : unit -> constr list
 
-val setoid_replace : constr -> constr -> constr option -> tactic
+val setoid_replace : constr -> constr -> tactic
 
 val setoid_rewriteLR : constr -> tactic