diff options
| author | herbelin | 2009-10-25 07:36:43 +0000 |
|---|---|---|
| committer | herbelin | 2009-10-25 07:36:43 +0000 |
| commit | b02da518c51456b003c61f9775050fbfe6090629 (patch) | |
| tree | fd9d603b8829a6dfa1190ae111e84b136be59060 /tactics | |
| parent | 28623d59a6381c7fb1c198ddca2dc382ba5c0e4c (diff) | |
Improved the treatment of Local/Global options (noneffective Local on
Implicit Arguments, Arguments Scope and Coercion fixed, noneffective
Global in sections for Hints and Notation detected).
Misc. improvements (comments + interpretation of Hint Constructors +
dev printer for hint_db).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index fafc0b5920..dd11e1ef0e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -465,6 +465,16 @@ let subst_autohint (subst,(local,name,hintlist as obj)) = let classify_autohint ((local,name,hintlist) as obj) = if local or hintlist = (AddTactic []) then Dispose else Substitute obj +let discharge_autohint (_,(local,name,hintlist as obj)) = + if local then None else + match hintlist with + | CreateDB _ -> + (* We assume that the transparent state is either empty or full *) + Some obj + | AddTransparency _ | AddTactic _ -> + (* Needs the adequate code here to support Global Hints in sections *) + None + let (inAutoHint,_) = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; @@ -560,7 +570,7 @@ let interp_hints h = HintsTransparencyEntry (List.map fr lhints, b) | HintsConstructors lqid -> let constr_hints_of_ind qid = - let ind = global_inductive qid in + let ind = global_inductive_with_alias qid in list_tabulate (fun i -> None, true, mkConstruct (ind,i+1)) (nconstructors ind) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) |