Change [Hints Resolve] to still accept constrs as arguments

to maintain compatibility, the term is then declared as a constant internally.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15948 85f007b7-540e-0410-9357-904b9bb8a0f7

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) =

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

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

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) ->

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