Switched to "standardized" names for the properties of eq and

identity. Add notations for compatibility and support for
understanding these notations in the ml files.



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

14 files changed, 76 insertions, 50 deletions

diff --git a/CHANGES b/CHANGES
index 85ed627e1..cd8ac1562 100644
--- a/CHANGES
+++ b/CHANGES
@@ -304,6 +304,9 @@ Tactics
 - New tactic "instantiate" (without argument).
 - Tactic firstorder "with" and "using" options have their meaning swapped for
   consistency with auto/eauto (source of incompatibility).
+- Tactic "intuition" now preserves inner "iff" (exceptional source of 
+  incompatibilities solvable by redefining "intuition" as 
+  "unfold iff in *; intuition".
 - Tactic "generalize" now supports "at" options to specify occurrences
   and "as" options to name the quantified hypotheses.
 - New tactic "specialize H with a" or "specialize (H a)" allows to transform
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index ef0ff426d..908267700 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -281,7 +281,7 @@ let constant = Coqlib.gen_constant "Fourier"
 
 (* Standard library *)
 open Coqlib
-let coq_sym_eqT = lazy (build_coq_sym_eq ())
+let coq_sym_eqT = lazy (build_coq_eq_sym ())
 let coq_False = lazy (build_coq_False ())
 let coq_not = lazy (build_coq_not ())
 let coq_eq = lazy (build_coq_eq ())
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index bb6aaea7d..eac109cae 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -837,7 +837,7 @@ let raw_polynom th op lc gl =
            (tclORELSE
               (tclORELSE
 		 (h_exact c'i_eq_c''i)
-		 (h_exact (mkApp(build_coq_sym_eq (),
+		 (h_exact (mkApp(build_coq_eq_sym (),
 				 [|th.th_a; c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHENS 
 		 (elim_type 
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 845707f9e..43c774707 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -15,6 +15,7 @@ open Term
 open Libnames
 open Pattern
 open Nametab
+open Syntax_def
 
 (************************************************************************)
 (* Generic functions to find Coq objects *)
@@ -25,10 +26,8 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
 let find_reference locstr dir s =
   let sp = Libnames.make_path (make_dir dir) (id_of_string s) in
-  try
-    Nametab.absolute_reference sp
-  with Not_found ->
-    anomaly (locstr^": cannot find "^(string_of_path sp))
+  try global_of_extended_global (Nametab.extended_absolute_reference sp)
+  with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp))
 
 let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
 let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s)
@@ -40,10 +39,14 @@ let has_suffix_in_dirs dirs ref =
   let dir = dirpath (sp_of_global ref) in
   List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
 
+let global_of_extended q =
+  try Some (global_of_extended_global q) with Not_found -> None
+
 let gen_constant_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let id = id_of_string s in
-  let all = Nametab.locate_all (make_short_qualid id) in
+  let all = Nametab.extended_locate_all (make_short_qualid id) in
+  let all = list_uniquize (list_map_filter global_of_extended all) in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
     | [x] -> constr_of_global x
@@ -195,12 +198,12 @@ let lazy_init_constant dir id = lazy (init_constant dir id)
 
 (* Equality on Set *)
 let coq_eq_eq = lazy_init_constant ["Logic"] "eq"
-let coq_eq_refl = lazy_init_constant ["Logic"] "refl_equal"
+let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl"
 let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind"
 let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec"
 let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect"
 let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
-let coq_eq_sym  = lazy_init_constant ["Logic"] "sym_eq"
+let coq_eq_sym  = lazy_init_constant ["Logic"] "eq_sym"
 let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
 
 let build_coq_eq_data () =
@@ -214,9 +217,11 @@ let build_coq_eq_data () =
   sym = Lazy.force coq_eq_sym }
 
 let build_coq_eq () = Lazy.force coq_eq_eq
-let build_coq_sym_eq () = Lazy.force coq_eq_sym
+let build_coq_eq_sym () = Lazy.force coq_eq_sym
 let build_coq_f_equal2 () = Lazy.force coq_f_equal2
 
+let build_coq_sym_eq = build_coq_eq_sym (* compatibility *)
+
 (* Specif *)
 let coq_sumbool  = lazy_init_constant ["Specif"] "sumbool"
 
@@ -228,8 +233,8 @@ let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity"
 let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind"
 let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
 let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
-let coq_identity_congr = lazy_init_constant ["Logic_Type"] "congr_id"
-let coq_identity_sym = lazy_init_constant ["Logic_Type"] "sym_id"
+let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr"
+let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym"
 
 let build_coq_identity_data () = {
   eq = Lazy.force coq_identity_eq;
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 038cf94ff..a4751f6e7 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -117,7 +117,7 @@ val build_coq_eq_data : coq_leibniz_eq_data delayed
 val build_coq_identity_data : coq_leibniz_eq_data delayed
 
 val build_coq_eq       : constr delayed (* = [(build_coq_eq_data()).eq] *)
-val build_coq_sym_eq   : constr delayed (* = [(build_coq_eq_data()).sym] *)
+val build_coq_eq_sym   : constr delayed (* = [(build_coq_eq_data()).sym] *)
 val build_coq_f_equal2 : constr delayed
 
 (* Specif *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 8f303ea61..bb8d68323 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -83,15 +83,19 @@ let declare_syntactic_definition local id onlyparse pat =
 let search_syntactic_definition loc kn =
   out_pat (KNmap.find kn !syntax_table)
 
-let locate_global_with_alias (loc,qid) =
-  match Nametab.extended_locate qid with
+let global_of_extended_global = function
   | TrueGlobal ref -> ref
   | SyntacticDef kn -> 
   match search_syntactic_definition dummy_loc kn with
   | [],ARef ref -> ref
-  | _ -> 
-      user_err_loc (loc,"",pr_qualid qid ++ 
-        str " is bound to a notation that does not denote a reference")
+  | _ -> raise Not_found
+
+let locate_global_with_alias (loc,qid) =
+  let ref = Nametab.extended_locate qid in
+  try global_of_extended_global ref
+  with Not_found ->
+    user_err_loc (loc,"",pr_qualid qid ++ 
+      str " is bound to a notation that does not denote a reference")
 
 let inductive_of_reference_with_alias r =
   match locate_global_with_alias (qualid_of_reference r) with
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 1599e844b..39583d856 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -32,9 +32,11 @@ val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation
 
 val locate_global_with_alias : qualid located -> global_reference
 
+(* Extract a global_reference from a reference that can be an "alias" *)
+val global_of_extended_global : extended_global_reference -> global_reference
+
 (* Locate a reference taking into account possible "alias" notations *)
 val global_with_alias : reference -> global_reference
 
 (* The same for inductive types *)
 val inductive_of_reference_with_alias : reference -> inductive
-
diff --git a/library/nametab.ml b/library/nametab.ml
index ac6c61116..5bb21b3e5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -419,12 +419,13 @@ let locate_mind qid =
     | TrueGlobal (IndRef (kn,0)) -> kn
     | _ -> raise Not_found
 
-
 let absolute_reference sp =
   match SpTab.find sp !the_ccitab with
     | TrueGlobal ref -> ref
     | _ -> raise Not_found
 
+let extended_absolute_reference sp = SpTab.find sp !the_ccitab
+
 let locate_in_absolute_module dir id =
   absolute_reference (make_path dir id)
 
diff --git a/library/nametab.mli b/library/nametab.mli
index eab86db1d..225a8b080 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -116,9 +116,10 @@ val locate_module : qualid -> module_path
 
 (* A variant looking up a [section_path] *)
 val absolute_reference : section_path -> global_reference
+val extended_absolute_reference : section_path -> extended_global_reference
 
 
-(*s These function tell if the given absolute name is already taken *)
+(*s These functions tell if the given absolute name is already taken *)
 
 val exists_cci : section_path -> bool
 val exists_modtype : section_path -> bool
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 259f51ad1..884a04e8f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -267,7 +267,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
   and t2 = pf_apply get_type_of gl c2 in
   if unsafe or (pf_conv_x gl t1 t2) then
     let e = build_coq_eq () in
-    let sym = build_coq_sym_eq () in
+    let sym = build_coq_eq_sym () in
     let eq = applist (e, [t1;c1;c2]) in
     tclTHENS (assert_as false None eq)
       [onLastHyp (fun id -> 
diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index ac8800923..64d5eb8af 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -522,8 +522,6 @@ Ltac ocaml_union_tac :=
   rewrite H; simpl; romega with *
  end.
 
-Import Logic. (* Unhide eq, otherwise Function complains. *)
-
 Function ocaml_union (s : t * t) { measure cardinal2 s } : t  :=
  match s with 
   | (Leaf, Leaf) => s#2
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index cb96f3f60..73e4924aa 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -114,8 +114,8 @@ Inductive Empty_set : Set :=.
     sole inhabitant is denoted [refl_identity A a] *)
 
 Inductive identity (A:Type) (a:A) : A -> Type :=
-  refl_identity : identity (A:=A) a a.
-Hint Resolve refl_identity: core.
+  identity_refl : identity a a.
+Hint Resolve identity_refl: core.
 
 Implicit Arguments identity_ind [A].
 Implicit Arguments identity_rec [A].
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index a91fd0480..ede73ebf1 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -243,7 +243,7 @@ End universal_quantification.
     [A] which is true of [x] is also true of [y] *)
 
 Inductive eq (A:Type) (x:A) : A -> Prop :=
-    refl_equal : x = x :>A
+    eq_refl : x = x :>A
 
 where "x = y :> A" := (@eq A x y) : type_scope.
 
@@ -255,7 +255,7 @@ Implicit Arguments eq_ind [A].
 Implicit Arguments eq_rec [A].
 Implicit Arguments eq_rect [A].
 
-Hint Resolve I conj or_introl or_intror refl_equal: core.
+Hint Resolve I conj or_introl or_intror eq_refl: core.
 Hint Resolve ex_intro ex_intro2: core.
 
 Section Logic_lemmas.
@@ -271,17 +271,17 @@ Section Logic_lemmas.
     Variable f : A -> B.
     Variables x y z : A.
 
-    Theorem sym_eq : x = y -> y = x.
+    Theorem eq_sym : x = y -> y = x.
     Proof.
       destruct 1; trivial.
     Defined.
-    Opaque sym_eq.
+    Opaque eq_sym.
 
-    Theorem trans_eq : x = y -> y = z -> x = z.
+    Theorem eq_trans : x = y -> y = z -> x = z.
     Proof.
       destruct 2; trivial.
     Defined.
-    Opaque trans_eq.
+    Opaque eq_trans.
 
     Theorem f_equal : x = y -> f x = f y.
     Proof.
@@ -289,30 +289,26 @@ Section Logic_lemmas.
     Defined.
     Opaque f_equal.
 
-    Theorem sym_not_eq : x <> y -> y <> x.
+    Theorem not_eq_sym : x <> y -> y <> x.
     Proof.
       red in |- *; intros h1 h2; apply h1; destruct h2; trivial.
     Qed.
 
-    Definition sym_equal := sym_eq.
-    Definition sym_not_equal := sym_not_eq.
-    Definition trans_equal := trans_eq.
-
   End equality.
 
   Definition eq_ind_r :
     forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
-    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+    intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
   Defined.
 
   Definition eq_rec_r :
     forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
-    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+    intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
   Defined.
 
   Definition eq_rect_r :
     forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
-    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+    intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
   Defined.
 End Logic_lemmas.
 
@@ -349,7 +345,18 @@ Proof.
   destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
 Qed.
 
-Hint Immediate sym_eq sym_not_eq: core.
+(* Aliases *)
+
+Notation sym_eq := eq_sym (only parsing).
+Notation trans_eq := eq_trans (only parsing).
+Notation sym_not_eq := not_eq_sym (only parsing).
+
+Notation refl_equal := eq_refl (only parsing).
+Notation sym_equal := eq_sym (only parsing).
+Notation trans_equal := eq_trans (only parsing).
+Notation sym_not_equal := not_eq_sym (only parsing).
+
+Hint Immediate eq_sym not_eq_sym: core.
 
 (** Basic definitions about relations and properties *)
 
@@ -411,7 +418,7 @@ intros A x y z H1 H2. rewrite <- H2; exact H1.
 Qed.
 
 Declare Left Step eq_stepl.
-Declare Right Step trans_eq.
+Declare Right Step eq_trans.
 
 Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
 Proof.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index f5cee92c7..bdec651da 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -29,22 +29,22 @@ Section identity_is_a_congruence.
 
  Variables x y z : A.
  
- Lemma sym_id : identity x y -> identity y x.
+ Lemma identity_sym : identity x y -> identity y x.
  Proof.
   destruct 1; trivial.
  Defined.
 
- Lemma trans_id : identity x y -> identity y z -> identity x z.
+ Lemma identity_trans : identity x y -> identity y z -> identity x z.
  Proof.
   destruct 2; trivial.
  Defined.
 
- Lemma congr_id : identity x y -> identity (f x) (f y).
+ Lemma identity_congr : identity x y -> identity (f x) (f y).
  Proof.
   destruct 1; trivial.
  Defined.
 
- Lemma sym_not_id : notT (identity x y) -> notT (identity y x).
+ Lemma not_identity_sym : notT (identity x y) -> notT (identity y x).
  Proof.
   red in |- *; intros H H'; apply H; destruct H'; trivial.
  Qed.
@@ -53,17 +53,22 @@ End identity_is_a_congruence.
 
 Definition identity_ind_r :
   forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
 Definition identity_rec_r :
   forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
 Definition identity_rect_r :
   forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
-Hint Immediate sym_id sym_not_id: core v62.
+Hint Immediate identity_sym not_identity_sym: core v62.
+
+Notation refl_id := identity_refl (only parsing).
+Notation sym_id := identity_sym (only parsing).
+Notation trans_id := identity_trans (only parsing).
+Notation sym_not_id := not_identity_sym (only parsing).