aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml4
-rw-r--r--parsing/g_vernac.ml43
-rw-r--r--parsing/ppvernac.ml3
-rw-r--r--tactics/tacinterp.ml13
-rw-r--r--theories/Classes/Init.v2
-rw-r--r--theories/Classes/SetoidClass.v28
-rw-r--r--theories/Classes/SetoidDec.v18
-rw-r--r--toplevel/classes.ml70
-rw-r--r--toplevel/classes.mli2
-rw-r--r--toplevel/vernacentries.ml6
-rw-r--r--toplevel/vernacexpr.ml2
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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 04:00:13 +0000