diff options
| author | Pierre-Marie Pédrot | 2017-09-05 00:42:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 01:06:23 +0200 |
| commit | da28b6e65d9b9a74c277cb15055131c8a151bb72 (patch) | |
| tree | 38697f7a7ddebd9006bae72405131fe906c83a85 /src/tac2quote.ml | |
| parent | ebe95a28cf012aff33eb5ce167be6520e6643cfd (diff) | |
Quotations for auto-related tactics.
Diffstat (limited to 'src/tac2quote.ml')
| -rw-r--r-- | src/tac2quote.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/tac2quote.ml b/src/tac2quote.ml index ed4cef2e2a..f87985435c 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -305,6 +305,10 @@ let of_strategy_flag (loc, flag) = std_proj "rConst", of_list ?loc of_reference flag.rConst; ]) +let of_hintdb (loc, hdb) = match hdb with +| QHintAll -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) None +| QHintDbs ids -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) (Some ids) + let pattern_vars pat = let rec aux () accu pat = match pat.CAst.v with | Constrexpr.CPatVar id -> Id.Set.add id accu |