Change notation for setoid inequality, coerce objects before comparing them. Debug tactic redefinition code, streamline Instantiation Tactic implementation using that. Have to adapt obligations tactic still.

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

11 files changed, 49 insertions, 102 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 5e82b85bce..6cc7942f8e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -360,6 +360,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b)
    | CLetIn(_, v, a, b) -> 
        CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b)
+   | CLetPattern(_, v, a, b) -> 
+       error "TODO: xlate_formula let | pattern"
    | CAppExpl(_, (Some n, r), l) -> 
        let l', last = decompose_last l in
 	 CT_proj(xlate_formula last,
@@ -2081,7 +2083,7 @@ let rec xlate_vernac =
         xlate_class id2, xlate_class id3)
 
     (* TypeClasses *) 
-   | VernacSetInstantiationTactic _|VernacDeclareInstance _|VernacContext _|
+   | VernacDeclareInstance _|VernacContext _|
 	 VernacInstance (_, _, _)|VernacClass (_, _, _, _, _) ->
 	   xlate_error "TODO: Type Classes commands"
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b69a6a97ac..dacfd7329a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -495,9 +495,6 @@ GEXTEND Gram
 
       | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
 
-      | IDENT "Instantiation"; IDENT "Tactic"; ":="; tac = Tactic.tactic -> 
-	  VernacSetInstantiationTactic tac
-
       (* Implicit *)
       | IDENT "Implicit"; IDENT "Arguments"; enrich = [ IDENT "Enriching" -> true | -> false ];
 	 (local,qid,pos) = 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e2653a9606..3502a9e86c 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -717,9 +717,6 @@ let rec pr_vernac = function
  | VernacDeclareInstance id ->
      hov 1 (str"Instance" ++ spc () ++ pr_lident id)
        
- | VernacSetInstantiationTactic tac ->
-     hov 1 (str"Instantiation Tactic :=" ++ spc () ++ pr_raw_tactic tac)
-
   (* Modules and Module Types *)
   | VernacDefineModule (export,m,bl,ty,bd) ->
       let b = pr_module_binders_list bl pr_lconstr in 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index dbb4648bc8..0a600bc64a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2593,6 +2593,7 @@ let load_md i ((sp,kn),defs) =
 	    Nametab.push_tactic (Until i) sp kn;
 	    add (kn,t)
       | UpdateTac kn ->
+	  mactab := Gmap.remove kn !mactab;
 	  add (kn,t)) defs
     
 let open_md i((sp,kn),defs) =
@@ -2604,12 +2605,20 @@ let open_md i((sp,kn),defs) =
 	  let sp = Libnames.make_path dp id in
 	  let kn = Names.make_kn mp dir (label_of_id id) in
 	    Nametab.push_tactic (Exactly i) sp kn
-      | UpdateTac kn -> ()) defs
+      | UpdateTac kn -> 
+	  let (path, id) = decode_kn kn in
+	  let sp = Libnames.make_path path id in
+	  Nametab.push_tactic (Exactly i) sp kn) defs
 
 let cache_md x = load_md 1 x
 
+let subst_kind subst id = 
+  match id with
+    | NewTac _ -> id
+    | UpdateTac kn -> UpdateTac (Mod_subst.subst_kn subst kn)
+
 let subst_md (_,subst,defs) =
-  List.map (fun (id,t) -> (id,subst_tactic subst t)) defs
+  List.map (fun (id,t) -> (subst_kind subst id,subst_tactic subst t)) defs
 
 let (inMD,outMD) =
   declare_object {(default_object "TAC-DEFINITION") with
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 3070053822..b5352e720a 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -1 +1 @@
-Instantiation Tactic := eauto 50 with typeclass_instances || eauto.
+Ltac typeclass_instantiation := eauto 50 with typeclass_instances || eauto.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index c3f2413073..adfd1c3a3f 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -33,15 +33,17 @@ Class Setoid (carrier : Type) (equiv : relation carrier) :=
 
 Definition equiv [ Setoid A R ] : _ := R.
 
-Infix "==" := equiv (at level 70, no associativity) : type_scope.
+(** Subset objects will be first coerced to their underlying type. *)
 
-Notation " x =!= y " := (~ x == y) (at level 70, no associativity).
+Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope.
+
+Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
 
 Definition equiv_refl [ s : Setoid A R ] : forall x : A, R x x := equiv_refl _ _ equiv_prf.
 Definition equiv_sym [ s : Setoid A R ] : forall x y : A, R x y -> R y x := equiv_sym _ _ equiv_prf.
 Definition equiv_trans [ s : Setoid A R ] : forall x y z : A, R x y -> R y z -> R x z := equiv_trans _ _ equiv_prf.
 
-Lemma nequiv_sym : forall [ s : Setoid A R ] (x y : A), x =!= y -> y =!= x.
+Lemma nequiv_sym : forall [ s : Setoid A R ] (x y : A), x =/= y -> y =/= x.
 Proof.
   intros ; red ; intros.
   apply equiv_sym in H0...
@@ -89,13 +91,13 @@ Ltac trans y := do_setoid_trans y.
 Ltac setoid_refl :=
   match goal with
     | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
-    | [ H : ?X =!= ?X |- _ ] => elim H ; setoid_refl
+    | [ H : ?X =/= ?X |- _ ] => elim H ; setoid_refl
   end.
 
 Ltac setoid_sym := 
   match goal with
     | [ H : ?X == ?Y |- ?Y == ?X ] => apply (equiv_sym (x:=X) (y:=Y) H)
-    | [ H : ?X =!= ?Y |- ?Y =!= ?X ] => apply (nequiv_sym (x:=X) (y:=Y) H)
+    | [ H : ?X =/= ?Y |- ?Y =/= ?X ] => apply (nequiv_sym (x:=X) (y:=Y) H)
   end.
 
 Ltac setoid_trans := 
@@ -107,7 +109,7 @@ Ltac setoid_trans :=
 
 Ltac setoid_tac := setoid_refl || setoid_sym || setoid_trans.
 
-Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =!= y -> y == z -> x =!= z.
+Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
 Proof.
   intros; intro. 
   assert(z == y) by setoid_sym.
@@ -115,7 +117,7 @@ Proof.
   contradiction.
 Qed.
 
-Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =!= z -> x =!= z.
+Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
   assert(y == x) by setoid_sym.
@@ -129,19 +131,19 @@ Open Scope type_scope.
 (* Ltac setoid_sat ::= *)
 (*   match goal with *)
 (*     | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *)
-(*     | [ H : ?x =!= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *)
+(*     | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *)
 (*     | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *)
-(*     | [ H : ?x == ?y, H' : ?y =!= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *)
-(*     | [ H : ?x =!= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *)
+(*     | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *)
+(*     | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *)
 (*   end. *)
 
 Ltac setoid_sat :=
   match goal with
     | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H)
-    | [ H : ?x =!= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H)
+    | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H)
     | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H')
-    | [ H : ?x == ?y, H' : ?y =!= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H')
-    | [ H : ?x =!= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H')
+    | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H')
+    | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H')
   end.
 
 Ltac setoid_saturate := repeat setoid_sat.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index a9f2ae6de9..d20b3df55f 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -18,31 +18,37 @@
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Require Import Coq.Classes.SetoidClass.
+(** Export notations. *)
 
+Require Export Coq.Classes.SetoidClass.
 
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
 Class [ Setoid A R ] => EqDec :=
-  equiv_dec : forall x y : A, { x == y } + { x =!= y }.
+  equiv_dec : forall x y : A, { x == y } + { x =/= y }.
 
 (** 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. *)
 
-Infix "==" := equiv_dec (no associativity, at level 70).
+Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
 
 (** Use program to solve some obligations. *)
 
+Definition swap_sumbool `A B` (x : { A } + { B }) : { B } + { A } :=
+  match x with
+    | left H => right _ H 
+    | right H => left _ H 
+  end.
+
 Require Import Coq.Program.Program.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { x =!= y } + { x == y } :=
-  if x == y then right else left.
+Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
 
 (** Overloaded notation for inequality. *)
 
-Infix "=!=" := nequiv_dec (no associativity, at level 70).
+Infix "=/=" := nequiv_dec (no associativity, at level 70).
 
 (** Define boolean versions, losing the logical information. *)
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 3eb9a30894..b3b7089cde 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -476,74 +476,18 @@ let context l =
       Command.declare_one_assumption false (Local (* global *), Definitional) t false (* inline *) (dummy_loc, id))
       (List.rev fullctx)
 
-(* let init     () = hints := [] *)
-(* let freeze   () = !hints *)
-(* let unfreeze fs = hints := fs *)
-
-(* let _ = Summary.declare_summary "hints db" *)
-(* 	  { Summary.freeze_function   = freeze; *)
-(* 	    Summary.unfreeze_function = unfreeze; *)
-(* 	    Summary.init_function     = init; *)
-(* 	    Summary.survive_module = false; *)
-(* 	    Summary.survive_section   = true } *)
-
 open Libobject
 
-(* let cache (_, db) := hints := db *)
-
-(* let (input,output) =  *)
-(*   declare_object *)
-(*     { (default_object "hints db") with *)
-(*       cache_function = cache; *)
-(*       load_function = (fun _ -> cache); *)
-(*       open_function = (fun _ -> cache); *)
-(*       classify_function = (fun (_,x) -> Keep x); *)
-(*       export_function = (fun x -> Some x) } *)
-
-let tactic = ref Tacticals.tclIDTAC
-let tactic_expr = ref (Obj.magic ())
-
-let set_instantiation_tactic t = 
-  tactic := Tacinterp.interp t; tactic_expr := t
-
-let freeze () = !tactic_expr
-let unfreeze t = set_instantiation_tactic t
-let init () =  
-  set_instantiation_tactic (Tacexpr.TacId[]) 
-
-let cache (_, tac) =
-  set_instantiation_tactic tac
-
-let _ = 
-  Summary.declare_summary "typeclasses instantiation tactic"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = true;
-      Summary.survive_section = true }
-
-let (input,output) = 
-  declare_object
-    { (default_object "type classes instantiation tactic state") with
-      cache_function = cache;
-      load_function = (fun _ -> cache);
-      open_function = (fun _ -> cache);
-      classify_function = (fun (_,x) -> Keep x);
-      export_function = (fun x -> Some x) }
-
-let set_instantiation_tactic t = 
-  Lib.add_anonymous_leaf (input t)
+let module_qualid = qualid_of_dirpath (dirpath_of_string "Coq.Classes.Init")
+let tactic_qualid = make_qualid (dirpath_of_string "Coq.Classes.Init") (id_of_string "typeclass_instantiation")
   
+let tactic_expr = Tacexpr.TacArg (Tacexpr.Reference (Qualid (dummy_loc, tactic_qualid)))
+let tactic = lazy (Library.require_library [(dummy_loc, module_qualid)] None;
+		   Tacinterp.interp tactic_expr)
 
-let initialize () =
-  if !tactic_expr = Tacexpr.TacId [] then
-    let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string "Coq.Classes.Init")) in
-      Library.require_library [qualid] None
-    
 let _ =
   Typeclasses.solve_instanciation_problem :=
-    (fun env -> initialize ();
-      fun evd ev evi -> 
-	solve_by_tac env evd ev evi !tactic)
+    (fun env evd ev evi -> 
+	solve_by_tac env evd ev evi (Lazy.force tactic))
       
     
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 7956089777..6444fb3d9a 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -51,8 +51,6 @@ val add_instance_hint : identifier -> unit
 
 val declare_instance : identifier located -> unit
 
-val set_instantiation_tactic : Tacexpr.raw_tactic_expr -> unit
-
 val mismatched_params : env -> constr_expr list -> named_context -> 'a
 
 val mismatched_props : env -> constr_expr list -> named_context -> 'a
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0aea24d47d..fed36d0049 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -535,10 +535,6 @@ let vernac_context l =
 let vernac_declare_instance id =
   Classes.declare_instance id
 
-(* Default tactics for solving evars management. *)
-let vernac_set_instantiation_tac tac =
-  Classes.set_instantiation_tactic tac
-
 (***********)
 (* Solving *)
 let vernac_solve n tcom b =
@@ -1222,8 +1218,6 @@ let interp c = match c with
   | VernacContext sup -> vernac_context sup
   | VernacDeclareInstance id -> vernac_declare_instance id
 
-  | VernacSetInstantiationTactic (tac) -> vernac_set_instantiation_tac tac
-
   (* Solving *)
   | VernacSolve (n,tac,b) -> vernac_solve n tac b
   | VernacSolveExistential (n,c) -> vernac_solve_existential n c
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index b2b648a665..cd9adf5cd9 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -242,8 +242,6 @@ type vernac_expr =
   | VernacDeclareInstance of
       lident (* instance name *)
 
-  | VernacSetInstantiationTactic of raw_tactic_expr
-
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident * 
       module_binder list * (module_type_ast * bool)