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

1 files changed, 24 insertions, 6 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index b20caf4501..97c954b8af 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