diff options
| author | msozeau | 2008-09-14 18:23:59 +0000 |
|---|---|---|
| committer | msozeau | 2008-09-14 18:23:59 +0000 |
| commit | a49d5036279440e6c35e54eda05f425696aba8ca (patch) | |
| tree | 218d86fc456e0dd40f01e868d8fd34b4ea114f22 /parsing | |
| parent | 3c8057d3c28b9243328ecb1f0a8197b11cf9fd77 (diff) | |
Add user syntax for creating hint databases [Create HintDb foo
[discriminated]] with a switch for using the more experimantal dnet impl
for every hint. Also add [Hint Transparent/Opaque] which parameterize
the dnet and the unification flags used by auto/eauto with a particular
database. Document all this. Remove [Typeclasses unfold] directives that
are no longer needed (everything is unfoldable by default) and move to
[Typeclasses Transparent/Opaque] syntax.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11409 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 5 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 2 |
2 files changed, 7 insertions, 0 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 5e0cc5d45c..35f02237aa 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -90,6 +90,9 @@ GEXTEND Gram | IDENT "Go"; IDENT "next" -> VernacGo GoNext | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) + | IDENT "Create"; local = locality; IDENT "HintDb" ; + id = IDENT ; b = [ "discriminated" -> true | -> false ] -> + VernacCreateHintDb (local, id, b) | IDENT "Hint"; local = locality; h = hint; dbnames = opt_hintbases -> VernacHints (local,dbnames, h) @@ -108,6 +111,8 @@ GEXTEND Gram [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] -> HintsResolve (List.map (fun x -> (n, true, x)) lc) | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc + | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) + | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index ced2700fd7..3a9de47d80 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -810,6 +810,8 @@ let rec pr_vernac = function hov 1 ((str "Ltac ") ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) + | VernacCreateHintDb (local,dbname,b) -> + hov 1 (str "Create " ++ pr_locality local ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ())) | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr pr_pattern_expr | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) -> |