Rename obligations_tactic to obligation_tactic and fix bugs #1893.

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

11 files changed, 55 insertions, 62 deletions

diff --git a/CHANGES b/CHANGES
index 675db3f185..e4dd9cbff9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -290,6 +290,7 @@ Program
   which argument decreases structurally.
 - Program Lemma, Axiom etc... now permit to have obligations in the statement 
   iff they can be automatically solved by the default tactic.
+- Renamed "Obligations Tactic" command to "Obligation Tactic".
 - New command "Preterm [ of id ]" to see the actual term fed to Coq for
   debugging purposes.
 - New option "Transparent Obligations" to control the declaration of 
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 46bc1a0b86..5cd9151f0c 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -139,10 +139,10 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
     END
 
 VERNAC COMMAND EXTEND Subtac_Set_Solver
-| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ 
+| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ 
     Coqlib.check_required_library ["Coq";"Program";"Tactics"];
     Tacinterp.add_tacdef false 
-      [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ]
+      [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligation_tactic"), true, t)] ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 55cdc7c4e1..4e824921bd 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -119,7 +119,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 let freeze () = !from_prg, !default_tactic_expr
 let unfreeze (v, t) = from_prg := v; set_default_tactic t
 let init () =
-  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligations_tactic" [])
+  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligation_tactic" [])
 
 let _ = 
   Summary.declare_summary "program-tcc-table"
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 0f6a5cbf6c..3580684a73 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -207,7 +207,7 @@ obligations (e.g. when defining mutually recursive blocks). The optional
 tactic is replaced by the default one if not specified.
 
 \begin{itemize}
-\item {\tt Obligations Tactic := \tacexpr}\comindex{Obligations Tactic}
+\item {\tt Obligation Tactic := \tacexpr}\comindex{Obligation Tactic}
   Sets the default obligation
   solving tactic applied to all obligations automatically, whether to
   solve them or when starting to prove one, e.g. using {\tt Next}.
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8428560665..329284136d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -76,14 +76,9 @@ let elimination_sort_of_clause = function
 
 (* 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
+  Approach is to break everything, if [eq] appears in head position 
+  then regular rewrite else try setoid rewrite. 
+  If occurrences are set, use setoid_rewrite.
 *)
 
 let general_s_rewrite_clause = function
@@ -95,43 +90,37 @@ let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause
 
 let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl =
   let ctype = pf_apply get_type_of gl c in 
-  (* 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_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] 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 ctype in
-	match match_with_equation t with
-	  | None -> 
-	      if l = NoBindings
-	      then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
-	      else error "The term provided does not end with an equation" 
-	  | Some (hdcncl,_) -> 
-	      if occs <> all_occurrences then (
-		!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl)
-	      else
-		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 
-		  try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
-		  with e -> 
-		    let eq = build_coq_eq () in
-		      if not (eq_constr eq head) then
-			try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
-			with _ -> raise e
-		      else raise e
-			
+  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_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
+	else error "The term provided does not end with an equation" 
+    | Some (hdcncl,_) -> 
+	if occs <> all_occurrences then (
+	  !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl)
+	else
+	  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 
+	    try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
+	    with e -> 
+	      let eq = build_coq_eq () in
+	      let t = snd (decompose_prod (whd_betaiotazeta ctype)) in 
+	      let head = if isApp t then fst (destApp t) else t in 
+		if not (eq_constr eq head) then
+		  try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
+		  with _ -> raise e
+		else raise e
+		  
 let general_rewrite_ebindings = 
   general_rewrite_ebindings_clause None
 let general_rewrite_bindings l2r occs (c,bl) = 
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index d96a532c3f..b530cc0989 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -40,7 +40,7 @@ Class [ equiv : Equivalence A ] => EqDec :=
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
    of [==] defined in the type scope, hence we can have both at the same time. *)
 
-Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
+Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope.
 
 Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
   match x with
@@ -58,7 +58,7 @@ Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x === y }
 
 (** Overloaded notation for inequality. *)
 
-Infix "=/=" := nequiv_dec (no associativity, at level 70).
+Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope.
 
 (** Define boolean versions, losing the logical information. *)
 
@@ -155,4 +155,4 @@ Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq :=
   Next Obligation.
   Proof. clear aux. red in H0. subst. 
     destruct y; intuition (discriminate || eauto).
-  Defined.
\ No newline at end of file
+  Defined.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 0d464b84e5..05167bdc58 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
+(* -*- coq-prog-name: "coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -434,6 +434,7 @@ Qed.
 Lemma morphism_releq_morphism [ Normalizes A R R', Morphism _ R' m ] : Morphism R m.
 Proof.
   intros.
+
   pose respect as r.
   pose normalizes as norm.
   setoid_rewrite norm.
@@ -464,4 +465,4 @@ Ltac morphism_reflexive :=
     | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
   end.
 
-Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
\ No newline at end of file
+Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 044195f194..31398aa3b9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *)
+(* -*- coq-prog-name: "coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -91,7 +91,7 @@ Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A)
     unfold complement.
     red. intros H.
     intros H' ; apply H'.
-    apply (reflexivity H).
+    apply reflexivity.
   Qed.
 
 
@@ -129,7 +129,7 @@ Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ intuition ]).
 
-Ltac obligations_tactic ::= simpl_relation.
+Ltac obligation_tactic ::= simpl_relation.
 
 (** Logical implication. *)
 
@@ -171,7 +171,7 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop :=
 
 (** An Equivalence is a PER plus reflexivity. *)
 
-Instance Equivalence_PER [ Equivalence A R ] : PER A R :=
+Instance Equivalence_PER [ Equivalence A R ] : PER A R | 10 :=
   PER_Symmetric := Equivalence_Symmetric ;
   PER_Transitive := Equivalence_Transitive.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index c5a8f3d308..227a932071 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -142,7 +142,7 @@ Program Instance type_equivalence : Equivalence Type type_eq.
 
 Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
 
-Ltac obligations_tactic ::= morphism_tac.
+Ltac obligation_tactic ::= morphism_tac.
 
 (** These are morphisms used to rewrite at the top level of a proof, 
    using [iff_impl_id_morphism] if the proof is in [Prop] and
@@ -178,4 +178,4 @@ Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
 
 (** Reset the default Program tactic. *)
 
-Ltac obligations_tactic ::= program_simpl.
+Ltac obligation_tactic ::= program_simpl.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index aea6f5d7ad..ff5f7cb6cd 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -174,3 +174,5 @@ Ltac default_add_morphism_tactic :=
   end.
 
 Ltac add_morphism_tactic := default_add_morphism_tactic.
+
+Ltac obligation_tactic ::= program_simpl.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 5182123f4e..45e965142d 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -222,7 +222,7 @@ Ltac refine_hyp c :=
     end.
 
 (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto]
-   is not enough, better rebind using [Obligations Tactic := tac] in this case, 
+   is not enough, better rebind using [Obligation Tactic := tac] in this case, 
    possibly using [program_simplify] to use standard goal-cleaning tactics. *)
 
 Ltac program_simplify :=
@@ -231,4 +231,4 @@ Ltac program_simplify :=
 
 Ltac program_simpl := program_simplify ; auto.
 
-Ltac obligations_tactic := program_simpl.
+Ltac obligation_tactic := program_simpl.