diff options
| author | Pierre-Marie Pédrot | 2020-03-12 15:31:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 11:57:19 +0100 |
| commit | d583f810be066929301864765601ff53497bc335 (patch) | |
| tree | 34ca12836c91fef1af681fec92b6ab45201c6b02 /tactics/hints.ml | |
| parent | 96ec58df041dc0111df0e681269aed9d0e9b571a (diff) | |
Export the user-facing attribute for hint locality.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 7cde342662..9c0cf03854 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1189,6 +1189,12 @@ let remove_hints local dbnames grs = (**************************************************************************) (* The "Hint" vernacular command *) (**************************************************************************) + +let check_no_export ~local ~superglobal () = + (* TODO: implement export for these entries *) + if not local && not superglobal then + CErrors.user_err Pp.(str "This command does not support the \"export\" attribute") + let add_resolves env sigma clist ~local ~superglobal dbnames = List.iter (fun dbname -> @@ -1208,14 +1214,16 @@ let add_unfolds l ~local ~superglobal dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_cuts l local dbnames = +let add_cuts l ~local ~superglobal dbnames = + let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> let hint = make_hint ~local dbname (AddCut l) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_mode l m local dbnames = +let add_mode l m ~local ~superglobal dbnames = + let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> let m' = make_mode l m in @@ -1223,7 +1231,8 @@ let add_mode l m local dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_transparency l b local dbnames = +let add_transparency l b ~local ~superglobal dbnames = + let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> let hint = make_hint ~local dbname (AddTransparency (l, b)) in @@ -1424,11 +1433,11 @@ let add_hints ~locality dbnames h = match h with | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local ~superglobal dbnames | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local ~superglobal dbnames - | HintsCutEntry lhints -> add_cuts lhints local dbnames - | HintsModeEntry (l,m) -> add_mode l m local dbnames + | HintsCutEntry lhints -> add_cuts lhints ~local ~superglobal dbnames + | HintsModeEntry (l,m) -> add_mode l m ~local ~superglobal dbnames | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames | HintsTransparencyEntry (lhints, b) -> - add_transparency lhints b local dbnames + add_transparency lhints b ~local ~superglobal dbnames | HintsExternEntry (info, tacexp) -> add_externs info tacexp ~local ~superglobal dbnames |