diff options
| author | filliatr | 1999-12-13 13:42:04 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-13 13:42:04 +0000 |
| commit | decb8c16274487ce3cac1e7d5de529b46b6d68e3 (patch) | |
| tree | 02a41980403e4c3fbeab8259a95ea14ba1b80e65 /tactics | |
| parent | 7dfacfe208a9fa5ad5f7669537c54609b4adf51e (diff) | |
- méthode load sur les Hints
- CAST pris en compte dans Astterm
- Coercin.lookup_path_to_sort_from protégé par un try/with
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@248 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 6358366b7b..46f2d340a3 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -166,7 +166,7 @@ let specification_autohint x = x let (inAutoHint,outAutoHint) = declare_object ("AUTOHINT", - { load_function = (fun _ -> ()); + { load_function = cache_autohint; cache_function = cache_autohint; open_function = (fun _ -> ()); specification_function = specification_autohint }) @@ -203,7 +203,7 @@ let make_apply_entry (eapply,verbose) name (c,cty) = if eapply & (nmiss <> 0) then begin if verbose then wARN [< 'sTR "the hint: EApply "; prterm c; - 'sTR " will only used by EAuto" >]; + 'sTR " will only be used by EAuto" >]; (hdconstr, { hname = name; pri = nb_hyp cty + nmiss; @@ -234,7 +234,7 @@ let make_resolves name eap (c,cty) = (* used to add an hypothesis to the local hint database *) let make_resolve_hyp hname htyp = try - [make_apply_entry (true, false) hname (mkVar hname, htyp)] + [make_apply_entry (true, Options.is_verbose()) hname (mkVar hname, htyp)] with | Failure _ -> [] | UserError _ -> anomaly "Papageno programme comme un blaireau" @@ -249,7 +249,8 @@ let add_resolves clist dbnames = (List.map (fun (name,c) -> let env = Global.env() in let ty = type_of env Evd.empty c in - make_resolves name (true,true) (c,ty)) clist)) + let verbose = Options.is_verbose() in + make_resolves name (true,verbose) (c,ty)) clist)) ))) dbnames @@ -730,7 +731,8 @@ let rec search_gen decomp n db_list local_db add_sign goal = let (hid,htyp) = hd_sign (pf_untyped_hyps g') in let hintl = try - [make_apply_entry (true,false) hid (mkVar hid,htyp)] + [make_apply_entry (true,Options.is_verbose()) + hid (mkVar hid,htyp)] with Failure _ -> [] in search_gen decomp n db_list |