diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-07 17:26:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-07 18:40:36 +0200 |
| commit | 38b34dfffcceab7fa7d5ba43c84e414d24cebe43 (patch) | |
| tree | c5449cf9c02c97586bf8a8edaa52d05d876d3e94 /tactics/extratactics.ml4 | |
| parent | 2313bde0116a5916912bebbaca77d291f7b2760a (diff) | |
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index cb15bb94c..342e65cba 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -325,11 +325,11 @@ let project_hint pri l2r r = in let ctx = Evd.universe_context_set sigma in let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in - (pri,false,true,Auto.PathAny, Auto.IsGlobRef (Globnames.ConstRef c)) + (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) let add_hints_iff l2r lc n bl = - Auto.add_hints true bl - (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc)) + Hints.add_hints true bl + (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc)) VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) |