diff options
| -rw-r--r-- | interp/smartlocate.ml | 1 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 8 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 10 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 8 | ||||
| -rw-r--r-- | tactics/auto.ml | 30 |
5 files changed, 44 insertions, 13 deletions
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index adf611b56..c5a28ab2d 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -25,6 +25,7 @@ let global_of_extended_global = function | SynDef kn -> match search_syntactic_definition kn with | [],NRef ref -> ref + | [],NApp (NRef ref,[]) -> ref | _ -> raise Not_found let locate_global_with_alias (loc,qid) = diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 97080fdad..f1eebc18e 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -102,9 +102,13 @@ type comment = | CommentString of string | CommentInt of int +type reference_or_constr = + | HintsReference of reference + | HintsConstr of constr_expr + type hints_expr = - | HintsResolve of (int option * bool * reference) list - | HintsImmediate of reference list + | HintsResolve of (int option * bool * reference_or_constr) list + | HintsImmediate of reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool | HintsConstructors of reference list diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index f2bf542ef..24efbcc5e 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -91,7 +91,7 @@ GEXTEND Gram VernacHints (enforce_module_locality local,dbnames, h) (* Declare "Resolve" explicitly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) - | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference; n = OPT natural; + | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; n = OPT natural; dbnames = opt_hintbases -> VernacHints (use_module_locality (),dbnames, HintsResolve (List.map (fun x -> (n, true, x)) lc)) @@ -100,10 +100,14 @@ GEXTEND Gram obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; + reference_or_constr: + [ [ r = global -> HintsReference r + | "("; c = operconstr LEVEL "200"; ")" -> HintsConstr c ] ] + ; hint: - [ [ IDENT "Resolve"; lc = LIST1 global; n = OPT natural -> + [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; n = OPT natural -> HintsResolve (List.map (fun x -> (n, true, x)) lc) - | IDENT "Immediate"; lc = LIST1 global -> HintsImmediate lc + | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8d763c2d1..476504549 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -179,17 +179,21 @@ let pr_opt_hintbases l = match l with | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z +let pr_reference_or_constr pr_c = function + | HintsReference r -> pr_reference r + | HintsConstr c -> pr_c c + let pr_hints local db h pr_c pr_pat = let opth = pr_opt_hintbases db in let pph = match h with | HintsResolve l -> str "Resolve " ++ prlist_with_sep sep - (fun (pri, _, c) -> pr_reference c ++ + (fun (pri, _, c) -> pr_reference_or_constr pr_c c ++ match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ()) l | HintsImmediate l -> - str"Immediate" ++ spc() ++ prlist_with_sep sep pr_reference l + str"Immediate" ++ spc() ++ prlist_with_sep sep (pr_reference_or_constr pr_c) l | HintsUnfold l -> str "Unfold " ++ prlist_with_sep sep pr_reference l | HintsTransparency (l, b) -> diff --git a/tactics/auto.ml b/tactics/auto.ml index b20caf450..97c954b8a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -815,18 +815,36 @@ let prepare_hint env (sigma,c) = mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in iter c -let interp_hints h = +let interp_hints = + let hint_counter = ref 1 in + fun h -> + let f c = + let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in + let c = prepare_hint (Global.env()) (evd,c) in + Evarutil.check_evars (Global.env()) Evd.empty evd c; + c in let fr r = let gr = global_with_alias r in let r' = evaluable_of_global_reference (Global.env()) gr in Dumpglob.add_glob (loc_of_reference r) gr; r' in - let fres (o, b, c) = - let gr = global_with_alias c in - (o, b, PathHints [gr], gr) in let fi c = - let gr = global_with_alias c in - PathHints [gr], gr + match c with + | HintsReference c -> + let gr = global_with_alias c in + (PathHints [gr], gr) + | HintsConstr c -> + let term = f c in + let id = id_of_string ("auto_hint_" ^ string_of_int !hint_counter) in + incr hint_counter; + let kn = Declare.declare_definition ~internal:Declare.KernelSilent + ~opaque:false id term in + let gr = ConstRef kn in + (PathHints [gr], gr) + in + let fres (o, b, c) = + let path, gr = fi c in + (o, b, path, gr) in let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in match h with |