diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-07 18:06:41 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-07 18:06:41 +0000 |
commit | 135c872c4a507726a633cc4025d284933fbc6660 (patch) | |
tree | ec7f8879f5ccc3ddb48f86fbc81509ada0895cc3 | |
parent | 4a1077f9d1ee00632ec72a4089013194f558cacd (diff) |
Add the ability to declare [Hint Extern]'s with no pattern.
This permits to create a database [relations] in [RelationClasses] with
a single extern tactic in it that tries to apply [reflexivity] or
[symmetry]. This is then automatically used in [auto with *] and repair
backward compatibility. The previous commit broke some scripts which were
using [intuition] to do (setoid) [reflexivity] or [symmetry]: this
worked only by accident, because the hint database of typeclasses was
used. Overrall, this also allows to put a bunch of
always-applicable, related tactics in some database or to use
[Hint Extern] but match only on hypotheses.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11384 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/interface/ascent.mli | 2 | ||||
-rw-r--r-- | contrib/interface/blast.ml | 6 | ||||
-rw-r--r-- | contrib/interface/vtp.ml | 2 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 5 | ||||
-rw-r--r-- | parsing/g_proofs.ml4 | 2 | ||||
-rw-r--r-- | parsing/ppvernac.ml | 7 | ||||
-rw-r--r-- | tactics/auto.ml | 129 | ||||
-rw-r--r-- | tactics/auto.mli | 25 | ||||
-rw-r--r-- | tactics/class_tactics.ml4 | 3 | ||||
-rw-r--r-- | tactics/eauto.ml4 | 6 | ||||
-rw-r--r-- | theories/Classes/Equivalence.v | 8 | ||||
-rw-r--r-- | theories/Classes/RelationClasses.v | 10 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 2 |
13 files changed, 120 insertions, 87 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 323385233..2eb2c3812 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -76,7 +76,7 @@ and ct_COMMAND = | CT_go of ct_INT_OR_LOCN | CT_guarded | CT_hint_destruct of ct_ID * ct_INT * ct_DESTRUCT_LOCATION * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST - | CT_hint_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST + | CT_hint_extern of ct_INT * ct_FORMULA_OPT * ct_TACTIC_COM * ct_ID_LIST | CT_hintrewrite of ct_ORIENTATION * ct_FORMULA_NE_LIST * ct_ID * ct_TACTIC_COM | CT_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST | CT_hints_immediate of ct_FORMULA_NE_LIST * ct_ID_LIST diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index dcea487a9..ddedbb325 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -190,8 +190,7 @@ and e_my_find_search db_list local_db hdc concl = tclTHEN (unify_e_resolve (term,cl)) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] - | Extern tacast -> Auto.conclPattern concl - (Option.get p) tacast + | Extern tacast -> Auto.conclPattern concl p tacast in (free_try tac,fmt_autotactic t)) (*i @@ -406,8 +405,7 @@ and my_find_search db_list local_db hdc concl = (unify_resolve st (term,cl)) (trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] - | Extern tacast -> - conclPattern concl (Option.get p) tacast)) + | Extern tacast -> conclPattern concl p tacast)) tacl and trivial_resolve db_list local_db cl = diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 551ad3a33..946090099 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -246,7 +246,7 @@ and fCOMMAND = function fNODE "hint_destruct" 6 | CT_hint_extern(x1, x2, x3, x4) -> fINT x1 ++ - fFORMULA x2 ++ + fFORMULA_OPT x2 ++ fTACTIC_COM x3 ++ fID_LIST x4 ++ fNODE "hint_extern" 4 diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 0516bd551..11d8d7a0b 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1751,7 +1751,10 @@ let rec xlate_vernac = CT_hints(CT_ident "Constructors", CT_id_ne_list(n1, names), dblist) | HintsExtern (n, c, t) -> - CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist) + let pat = match c with + | None -> CT_coerce_ID_OPT_to_FORMULA_OPT (CT_coerce_NONE_to_ID_OPT CT_none) + | Some c -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula c) + in CT_hint_extern(CT_int n, pat, xlate_tactic t, dblist) | HintsImmediate l -> let f1, formulas = match List.map xlate_formula l with a :: tl -> a, tl diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 486f80abc..5e0cc5d45 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -110,7 +110,7 @@ GEXTEND Gram | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc - | IDENT "Extern"; n = natural; c = constr_pattern ; "=>"; + | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; tac = tactic -> HintsExtern (n,c,tac) | IDENT "Destruct"; diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 646f697b6..ced2700fd 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -204,9 +204,10 @@ let pr_hints local db h pr_c pr_pat = pr_reference l | HintsConstructors c -> str"Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c - | HintsExtern (n,c,tac) -> - str "Extern" ++ spc() ++ int n ++ spc() ++ pr_pat c ++ str" =>" ++ - spc() ++ pr_raw_tactic tac + | HintsExtern (n,c,tac) -> + let pat = match c with None -> mt () | Some pat -> pr_pat pat in + str "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ + spc() ++ pr_raw_tactic tac | HintsDestruct(name,i,loc,c,tac) -> str "Destruct " ++ pr_id name ++ str" :=" ++ spc() ++ hov 0 (int i ++ spc() ++ pr_destruct_location loc ++ spc() ++ diff --git a/tactics/auto.ml b/tactics/auto.ml index a5778d45d..58730d5d1 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -59,6 +59,8 @@ type pri_auto_tactic = { code : auto_tactic (* the tactic to apply when the concl matches pat *) } +type hint_entry = global_reference option * pri_auto_tactic + let pri_ord {pri=pri1} {pri=pri2} = pri1 - pri2 let pri_order {pri=pri1} {pri=pri2} = pri1 <= pri2 @@ -121,14 +123,15 @@ module Hint_db = struct hintdb_state : Names.transparent_state; use_dn : bool; hintdb_map : search_entry Constr_map.t; - (* A list of unindexed entries starting with an unfoldable constant. *) - hintdb_transp : stored_data list + (* A list of unindexed entries starting with an unfoldable constant + or with no associated pattern. *) + hintdb_nopat : stored_data list } let empty st use_dn = { hintdb_state = st; use_dn = use_dn; hintdb_map = Constr_map.empty; - hintdb_transp = [] } + hintdb_nopat = [] } let find key db = try Constr_map.find key db.hintdb_map @@ -136,12 +139,12 @@ module Hint_db = struct let map_all k db = let (l,l',_) = find k db in - Sort.merge pri_order (db.hintdb_transp @ l) l' + Sort.merge pri_order (db.hintdb_nopat @ l) l' let map_auto (k,c) db = let st = if db.use_dn then Some db.hintdb_state else None in let l' = lookup_tacs (k,c) st (find k db) in - Sort.merge pri_order db.hintdb_transp l' + Sort.merge pri_order db.hintdb_nopat l' let is_exact = function | Give_exact _ -> true @@ -160,26 +163,34 @@ module Hint_db = struct | EvalConstRef cst -> (ids, Cpred.add cst csts)), true | _ -> db.hintdb_state, false in - let dnst, db = + let dnst, db, k = if db.use_dn then - let db' = - if rebuild then rebuild_db st' db + let db', k' = + if rebuild then rebuild_db st' db, k else (* not an unfold *) - if is_transparent_gr st' k && not (List.mem v db.hintdb_transp) then - { db with hintdb_transp = v :: db.hintdb_transp } - else db + (match k with + | Some gr -> db, if is_transparent_gr st' gr then None else k + | None -> db, None) in - (Some st', db') - else None, db + (Some st', db', k') + else None, db, k in - let oval = find k db in let pat = if not db.use_dn && is_exact v.code then None else v.pat in - { db with hintdb_map = Constr_map.add k (add_tac pat v dnst oval) db.hintdb_map; - hintdb_state = st' } + match k with + | None -> + if not (List.mem v db.hintdb_nopat) then + { db with hintdb_nopat = v :: db.hintdb_nopat } + else db + | Some gr -> + let oval = find gr db in + { db with hintdb_map = Constr_map.add gr (add_tac pat v dnst oval) db.hintdb_map; + hintdb_state = st' } let add_list l db = List.fold_right add_one l db - let iter f db = Constr_map.iter (fun k (l,l',_) -> f k (l@l')) db.hintdb_map + let iter f db = + f None db.hintdb_nopat; + Constr_map.iter (fun k (l,l',_) -> f (Some k) (l@l')) db.hintdb_map let transparent_state db = db.hintdb_state @@ -255,7 +266,7 @@ let make_exact_entry pri (c,cty) = let ce = mk_clenv_from dummy_goal (c,cty) in let c' = clenv_type ce in let pat = Pattern.pattern_of_constr c' in - (head_of_constr_reference (List.hd (head_constr cty)), + (Some (head_of_constr_reference (List.hd (head_constr cty))), { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c }) let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = @@ -269,7 +280,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = with BoundPattern -> failwith "make_apply_entry") in let nmiss = List.length (clenv_missing ce) in if nmiss = 0 then - (hd, + (Some hd, { pri = (match pri with None -> nb_hyp cty | Some p -> p); pat = Some pat; code = Res_pf(c,{ce with env=empty_env}) }) @@ -278,7 +289,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = if verbose then warn (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); - (hd, + (Some hd, { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); pat = Some pat; code = ERes_pf(c,{ce with env=empty_env}) }) @@ -314,23 +325,23 @@ let make_resolve_hyp env sigma (hname,_,htyp) = (* REM : in most cases hintname = id *) let make_unfold (ref, eref) = - (ref, + (Some ref, { pri = 4; pat = None; code = Unfold_nth eref }) let make_extern pri pat tacast = - let hdconstr = try_head_pattern pat in + let hdconstr = Option.map try_head_pattern pat in (hdconstr, { pri=pri; - pat = Some pat; + pat = pat; code= Extern tacast }) let make_trivial env sigma c = let t = hnf_constr env sigma (type_of env sigma c) in let hd = head_of_constr_reference (List.hd (head_constr t)) in let ce = mk_clenv_from dummy_goal (c,t) in - (hd, { pri=1; + (Some hd, { pri=1; pat = Some (Pattern.pattern_of_constr (clenv_type ce)); code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) }) @@ -364,7 +375,7 @@ let add_transparency dbname grs b = type hint_action = | CreateDB of bool * transparent_state | AddTransparency of evaluable_global_reference list * bool - | AddTactic of (global_reference * pri_auto_tactic) list + | AddTactic of (global_reference option * pri_auto_tactic) list let cache_autohint (_,(local,name,hints)) = match hints with @@ -385,11 +396,15 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = code = code ; } in - let subst_hint (lab,data as hint) = - let lab',elab' = subst_global subst lab in - let lab' = - try head_of_constr_reference (List.hd (head_constr_bound elab' [])) - with Tactics.Bound -> lab' in + let subst_key gr = + let (lab'', elab') = subst_global subst gr in + let gr' = + (try head_of_constr_reference (List.hd (head_constr_bound elab' [])) + with Tactics.Bound -> lab'') + in if gr' == gr then gr else gr' + in + let subst_hint (k,data as hint) = + let k' = Option.smartmap subst_key k in let data' = match data.code with | Res_pf (c, clenv) -> let c' = subst_mps subst c in @@ -417,8 +432,8 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = if tac==tac' then data else trans_data data (Extern tac') in - if lab' == lab && data' == data then hint else - (lab',data') + if k' == k && data' == data then hint else + (k',data') in match hintlist with | CreateDB _ -> obj @@ -474,17 +489,22 @@ let add_transparency l b local dbnames = (inAutoHint (local,dbname, AddTransparency (l, b)))) dbnames -let add_extern pri (patmetas,pat) tacast local dbname = +let add_extern pri pat tacast local dbname = (* We check that all metas that appear in tacast have at least one occurence in the left pattern pat *) let tacmetas = [] in - match (list_subtract tacmetas patmetas) with - | i::_ -> - errorlabstrm "add_extern" - (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.") - | [] -> + match pat with + | Some (patmetas,pat) -> + (match (list_subtract tacmetas patmetas) with + | i::_ -> + errorlabstrm "add_extern" + (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.") + | [] -> + Lib.add_anonymous_leaf + (inAutoHint(local,dbname, AddTactic [make_extern pri (Some pat) tacast]))) + | None -> Lib.add_anonymous_leaf - (inAutoHint(local,dbname, AddTactic [make_extern pri pat tacast])) + (inAutoHint(local,dbname, AddTactic [make_extern pri None tacast])) let add_externs pri pat tacast local dbnames = List.iter (add_extern pri pat tacast local) dbnames @@ -548,8 +568,8 @@ let add_hints local dbnames0 h = add_resolves env sigma lcons local dbnames in List.iter add_one lqid | HintsExtern (pri, patcom, tacexp) -> - let pat = Constrintern.interp_constrpattern Evd.empty (Global.env()) patcom in - let tacexp = !forward_intern_tac (fst pat) tacexp in + let pat = Option.map (Constrintern.interp_constrpattern Evd.empty (Global.env())) patcom in + let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in add_externs pri pat tacexp local dbnames | HintsDestruct(na,pri,loc,pat,code) -> if dbnames0<>[] then @@ -648,9 +668,15 @@ let print_hint_db db = str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ())); Hint_db.iter (fun head hintlist -> - msg (hov 0 - (str "For " ++ pr_global head ++ str " -> " ++ - fmt_hint_list hintlist))) + match head with + | Some head -> + msg (hov 0 + (str "For " ++ pr_global head ++ str " -> " ++ + fmt_hint_list hintlist)) + | None -> + msg (hov 0 + (str "For any goal -> " ++ + fmt_hint_list hintlist))) db let print_hint_db_by_name dbname = @@ -728,10 +754,13 @@ let forward_interp_tactic = let set_extern_interp f = forward_interp_tactic := f let conclPattern concl pat tac gl = - let constr_bindings = - try matches pat concl - with PatternMatchingFailure -> error "conclPattern" in - !forward_interp_tactic constr_bindings tac gl + let constr_bindings = + match pat with + | None -> [] + | Some pat -> + try matches pat concl + with PatternMatchingFailure -> error "conclPattern" in + !forward_interp_tactic constr_bindings tac gl (**************************************************************************) (* The Trivial tactic *) @@ -779,7 +808,7 @@ and my_find_search_nodelta db_list local_db hdc concl = (trivial_fail_db false db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> - conclPattern concl (Option.get p) tacast)) + conclPattern concl p tacast)) tacl and my_find_search mod_delta = @@ -828,7 +857,7 @@ and my_find_search_delta db_list local_db hdc concl = (trivial_fail_db true db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> - conclPattern concl (Option.get p) tacast)) + conclPattern concl p tacast)) tacl and trivial_resolve mod_delta db_list local_db cl = diff --git a/tactics/auto.mli b/tactics/auto.mli index b35f98ec1..0eaa35872 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -44,6 +44,10 @@ type stored_data = pri_auto_tactic type search_entry = stored_data list * stored_data list * stored_data Btermdn.t +(* The head may not be bound. *) + +type hint_entry = global_reference option * pri_auto_tactic + module Hint_db : sig type t @@ -51,9 +55,9 @@ module Hint_db : val find : global_reference -> t -> search_entry val map_all : global_reference -> t -> pri_auto_tactic list val map_auto : global_reference * constr -> t -> pri_auto_tactic list - val add_one : global_reference * pri_auto_tactic -> t -> t - val add_list : (global_reference * pri_auto_tactic) list -> t -> t - val iter : (global_reference -> stored_data list -> unit) -> t -> unit + val add_one : hint_entry -> t -> t + val add_list : (hint_entry) list -> t -> t + val iter : (global_reference option -> stored_data list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state @@ -91,7 +95,7 @@ val print_hint_db_by_name : hint_db_name -> unit [c] is the term given as an exact proof to solve the goal; [ctyp] is the type of [c]. *) -val make_exact_entry : int option -> constr * constr -> global_reference * pri_auto_tactic +val make_exact_entry : int option -> constr * constr -> hint_entry (* [make_apply_entry (eapply,verbose) pri (c,cty)]. [eapply] is true if this hint will be used only with EApply; @@ -102,7 +106,7 @@ val make_exact_entry : int option -> constr * constr -> global_reference * pri_a val make_apply_entry : env -> evar_map -> bool * bool * bool -> int option -> constr * constr - -> global_reference * pri_auto_tactic + -> hint_entry (* A constr which is Hint'ed will be: (1) used as an Exact, if it does not start with a product @@ -113,7 +117,7 @@ val make_apply_entry : val make_resolves : env -> evar_map -> bool * bool * bool -> int option -> constr -> - (global_reference * pri_auto_tactic) list + hint_entry list (* [make_resolve_hyp hname htyp]. used to add an hypothesis to the local hint database; @@ -121,14 +125,13 @@ val make_resolves : If the hyp cannot be used as a Hint, the empty list is returned. *) val make_resolve_hyp : - env -> evar_map -> named_declaration -> - (global_reference * pri_auto_tactic) list + env -> evar_map -> named_declaration -> hint_entry list (* [make_extern pri pattern tactic_expr] *) val make_extern : - int -> constr_pattern -> Tacexpr.glob_tactic_expr - -> global_reference * pri_auto_tactic + int -> constr_pattern option -> Tacexpr.glob_tactic_expr + -> hint_entry val set_extern_interp : (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) -> unit @@ -163,7 +166,7 @@ val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the right values to build a tactic *) -val conclPattern : constr -> constr_pattern -> Tacexpr.glob_tactic_expr -> tactic +val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> tactic (* The Auto tactic *) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 3cdf050c4..e803e8dcb 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -143,8 +143,7 @@ and e_my_find_search db_list local_db hdc concl = tclTHEN (unify_e_resolve flags (term,cl)) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] - | Extern tacast -> conclPattern concl - (Option.get p) tacast + | Extern tacast -> conclPattern concl p tacast in (tac,b,fmt_autotactic t) in diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index eae6f5632..dcff75331 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -140,8 +140,7 @@ and e_my_find_search_nodelta db_list local_db hdc concl = tclTHEN (unify_e_resolve_nodelta (term,cl)) (e_trivial_fail_db false db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] - | Extern tacast -> conclPattern concl - (Option.get p) tacast + | Extern tacast -> conclPattern concl p tacast in (tac,fmt_autotactic t)) (*i @@ -179,8 +178,7 @@ and e_my_find_search_delta db_list local_db hdc concl = tclTHEN (unify_e_resolve st (term,cl)) (e_trivial_fail_db true db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] - | Extern tacast -> conclPattern concl - (Option.get p) tacast + | Extern tacast -> conclPattern concl p tacast in (tac,fmt_autotactic t)) (*i diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 03b0e9ad5..197786c8b 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -55,11 +55,6 @@ Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv. Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv. - Next Obligation. - Proof. - symmetry ; auto. - Qed. - Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv. Next Obligation. @@ -133,10 +128,7 @@ End Respecting. Program Instance pointwise_equivalence [ eqb : Equivalence B eqB ] : Equivalence (A -> B) (pointwise_relation eqB) | 9. - Solve Obligations using simpl_relation ; first [ reflexivity | (symmetry ; auto) ]. - Next Obligation. Proof. transitivity (y a) ; auto. Qed. - diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index cfcd93c0a..c1d7f34ce 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -59,6 +59,16 @@ Hint Resolve @irreflexivity : ord. Unset Implicit Arguments. +(** A HintDb for relations. *) + +Ltac solve_relation := + match goal with + | [ |- ?R ?x ?x ] => reflexivity + | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H + end. + +Hint Extern 4 => solve_relation : relations. + (** We can already dualize all these properties. *) Program Instance flip_Reflexive [ Reflexive A R ] : Reflexive (flip R) := diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index f87549706..989311404 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -117,7 +117,7 @@ type hints = | HintsUnfold of reference list | HintsTransparency of reference list * bool | HintsConstructors of reference list - | HintsExtern of int * constr_expr * raw_tactic_expr + | HintsExtern of int * constr_expr option * raw_tactic_expr | HintsDestruct of identifier * int * (bool,unit) location * constr_expr * raw_tactic_expr |