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

4 files changed, 7 insertions, 73 deletions

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)