- Patch sur "intros until 0"

- MAJ CHANGES et COMPATIBILITY
- Réservation de || et && dans Notations.v
- code mort et MAJ suite commit 11072 (tactics.ml et changes.txt)


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

7 files changed, 28 insertions, 37 deletions

diff --git a/CHANGES b/CHANGES
index 49fef1dd75..4271001293 100644
--- a/CHANGES
+++ b/CHANGES
@@ -109,7 +109,8 @@ Libraries (DOC TO CHECK)
   le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare 
   transparent, ...) (exceptional source of incompatibilities).
 - Boolean operators moved from module Bool to module Datatypes (may need
-  to rename qualified references in script)
+  to rename qualified references in script and force notations || and &&
+  to be at levels 50 and 40 respectively).
 - The constructors xI and xO of type positive now have postfix notations 
   "~1" and "~0", allowing to write numbers in binary form easily, for instance 
   6 is 1~1~0 and 4*p is p~0~0 (see BinPos.v).
@@ -244,6 +245,8 @@ Tactics
   matching lemma among the components of the conjunction; tactic apply also
   able to apply lemmas of conclusion an empty type.
 - Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)".
+- Tactic firstorder "with" and "using" options have their meaning swapped for
+  consistency with auto/eauto (source of incompatibility).
 - Tactic "generalize" now supports "at" options to specify occurrences
   and "as" options to name the hypothesis.
 - New tactic "specialize H with a" or "specialize (H a)" allows to transform
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 1ed4b25d0a..97963c8dca 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -3,15 +3,6 @@ Potential sources of incompatibilities between Coq V8.1 and V8.2
 
 (see also file CHANGES)
 
-Language
-
-- Constants hidding polymorphic inductive types are now polymorphic themselves.
-  This may exceptionally affect the naming of introduction hypotheses if such
-  an inductive type in Type is used on small types such as Prop or
-  Set: the hypothesis names suffix will default to H instead of X.  As
-  a matter of fact, it is recommended to systematically name the
-  hypotheses that are later refered to in the proof script.
-
 Tactics
 
 - The apply tactic now unfolds the constants if needed to succeed.  As
@@ -40,9 +31,25 @@ Tactics
   variable when perform introductions. Changing intros to the
   appropriate intro x x0 ... xn should fix the problem.
 
+- Tactic firstorder "with" and "using" options have their meaning
+  swapped for consistency with auto/eauto. The solution is to swap
+  the use of these options in call to firstorder.
+
+- Introduction patterns are more strict. In "intros [ ... | ... | ... ] H",
+  the names in the brackets are synchronized so that H denotes the same
+  hypothesis in every subgoal.
+
 - Some bug fixes may lead to incompatibilities (see CHANGES for a detailed
   account).
 
+Language
+
+- Constants hidding polymorphic inductive types are now polymorphic
+  themselves. This may exceptionally affect the naming of
+  introduction hypotheses if such an inductive type in Type is used on
+  small types such as Prop or Set: the hypothesis names suffix will
+  default to H instead of X.
+
 Libraries
 
 - Some changes in the library (as mentioned in the CHANGES file) may
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index b50a3d72bc..d8cdf738d9 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -9,8 +9,6 @@ A few differences in Coq ML interfaces between Coq V8.0 and V8.1
 
 Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply
 Tactics: apply_with_bindings -> apply_with_bindings_wo_evars
-Tactics: boolean argument of letin_tac changed its meaning (false now
-         means use Leibniz equality instead of a local definition)
 Eauto.simplest_apply -> Hiddentac.h_simplest_apply
 Evarutil.define_evar_as_arrow -> define_evar_as_product
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ba2d2fdf39..8d8a9950e3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -211,7 +211,7 @@ let lookup_index_as_renamed env t n =
 		   lookup (n-1) (d+1) c'
 	  )
     | Cast (c,_,_) -> lookup n d c
-    | _ -> None
+    | _ -> if n=0 then Some (d-1) else None
   in lookup n 1 t
 
 (**********************************************************************)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c81d7f3172..905511b120 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1154,28 +1154,6 @@ let generalize_goal gl i ((occs,c),na) cl =
   let na = generalized_name c t cl' na in
   mkProd (na,t,cl')
 
-(*
-  match kind_of_term cl with
-  | App (f,[|a|]) when isLambda f & eq_constr a c ->
-      (* Assume tactic pattern has been applied first *)
-      let na = match kind_of_term c with Var id -> Name id | _ -> Anonymous in
-      mkProd_name (pf_env gl) (na,t,mkApp (f,[|mkRel 1|]))
-  | _ ->
-    match kind_of_term c with
-    | Var id ->
-	(* The choice of remembering or not a non dependent name has an impact
-	   on the future Intro naming strategy! *)
-	(* if dependent c cl then mkNamedProd id t cl
-	   else mkProd (Anonymous,t,cl) *)
- 	mkNamedProd id t cl
-    | _        -> 
-        let cl' = subst_term c cl in
-        if noccurn 1 cl' then 
-	  mkProd (Anonymous,t,cl)
-        else
-	  mkProd_name (pf_env gl) (Anonymous, t, cl')
-*)
-
 let generalize_dep c gl =
   let env = pf_env gl in
   let sign = pf_hyps gl in
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index eb12be1a04..1e8a5b0621 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -48,8 +48,8 @@ Definition xorb (b1 b2:bool) : bool :=
 
 Definition negb (b:bool) := if b then false else true.
 
-Infix "||" := orb (at level 50, left associativity) : bool_scope.
-Infix "&&" := andb (at level 40, left associativity) : bool_scope.
+Infix "||" := orb : bool_scope.
+Infix "&&" := andb : bool_scope.
 
 (*******************************)
 (** * Properties of [andb]     *)
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 9a0406d591..c4780ace52 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -49,6 +49,11 @@ Reserved Notation "- x" (at level 35, right associativity).
 Reserved Notation "/ x" (at level 35, right associativity).
 Reserved Notation "x ^ y" (at level 30, right associativity).
 
+(** Notations for booleans *)
+
+Reserved Notation "x || y" (at level 50, left associativity).
+Reserved Notation "x && y" (at level 40, left associativity).
+
 (** Notations for pairs *)
 
 Reserved Notation "( x , y , .. , z )" (at level 0).