diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 70 | ||||
| -rw-r--r-- | toplevel/classes.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
4 files changed, 7 insertions, 73 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 3eb9a3089..b3b7089cd 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 795608977..6444fb3d9 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 0aea24d47..fed36d004 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 b2b648a66..cd9adf5cd 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) |