Fix #7812

3 files changed, 72 insertions, 19 deletions

diff --git a/doc/changelog/04-tactics/11883-fix-autounfold.rst b/doc/changelog/04-tactics/11883-fix-autounfold.rst
new file mode 100644
index 0000000000..83ff177380
--- /dev/null
+++ b/doc/changelog/04-tactics/11883-fix-autounfold.rst
@@ -0,0 +1,13 @@
+- **Fixed:**
+  The behavior of :tacn:`autounfold` no longer depends on the names of terms and modules
+  (`#11883 <https://github.com/coq/coq/pull/11883>`_,
+  fixes `#7812 <https://github.com/coq/coq/issues/7812>`_,
+  by Attila Gáspár).
+- **Changed:**
+  `at` clauses can no longer be used with :tacn:`autounfold`. Since they had no effect, it is safe to remove them
+  (`#11883 <https://github.com/coq/coq/pull/11883>`_,
+  by Attila Gáspár).
+- **Changed:**
+  :tacn:`autounfold` no longer fails when the :cmd:`Opaque` command is used on constants in the hint databases
+  (`#11883 <https://github.com/coq/coq/pull/11883>`_,
+  by Attila Gáspár).
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index a89e5ef19a..28b5ed5811 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -430,29 +430,39 @@ let make_dimension n = function
   | None -> (true,make_depth n)
   | Some d -> (false,d)
 
+let autounfolds ids csts gl cls =
+  let hyps = Tacmach.New.pf_ids_of_hyps gl in
+  let env = Tacmach.New.pf_env gl in
+  let ids = List.filter (fun id -> List.mem id hyps && Tacred.is_evaluable env (EvalVarRef id)) ids in
+  let csts = List.filter (fun cst -> Tacred.is_evaluable env (EvalConstRef cst)) csts in
+  let flags =
+    List.fold_left (fun flags cst -> CClosure.RedFlags.(red_add flags (fCONST cst)))
+      (List.fold_left (fun flags id -> CClosure.RedFlags.(red_add flags (fVAR id)))
+         CClosure.betaiotazeta ids) csts
+  in reduct_option ~check:false (Reductionops.clos_norm_flags flags, DEFAULTcast) cls
+
 let cons a l = a :: l
 
-let autounfolds db occs cls gl =
-  let unfolds = List.concat (List.map (fun dbname ->
-    let db = try searchtable_map dbname
-      with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname)
-    in
-    let (ids, csts) = Hint_db.unfolds db in
-    let hyps = pf_ids_of_hyps gl in
-    let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in
-      Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts
-        (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
-  in Proofview.V82.of_tactic (unfold_option unfolds cls) gl
+exception UnknownDatabase of string
 
 let autounfold db cls =
-  Proofview.V82.tactic begin fun gl ->
-  let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in
-  let tac = autounfolds db in
-  tclMAP (function
-    | OnHyp (id,occs,where) -> tac occs (Some (id,where))
-    | OnConcl occs -> tac occs None)
-    cls gl
-  end
+  if not (Locusops.clause_with_generic_occurrences cls) then
+    user_err ~hdr:"autounfold" (str "\"at\" clause not supported");
+  match List.fold_left (fun (ids, csts) dbname ->
+    let db = try searchtable_map dbname
+      with Not_found -> raise (UnknownDatabase dbname)
+    in
+    let (db_ids, db_csts) = Hint_db.unfolds db in
+    (Id.Set.fold cons db_ids ids, Cset.fold cons db_csts csts)) ([], []) db
+  with
+  | (ids, csts) -> Proofview.Goal.enter begin fun gl ->
+      let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
+      let tac = autounfolds ids csts gl in
+      Tacticals.New.tclMAP (function
+      | OnHyp (id, _, where) -> tac (Some (id, where))
+      | OnConcl _ -> tac None) cls
+    end
+  | exception UnknownDatabase dbname -> Tacticals.New.tclZEROMSG (str "Unknown database " ++ str dbname)
 
 let autounfold_tac db cls =
   Proofview.tclUNIT () >>= fun () ->
diff --git a/test-suite/bugs/closed/bug_7812.v b/test-suite/bugs/closed/bug_7812.v
new file mode 100644
index 0000000000..a714eea81d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_7812.v
@@ -0,0 +1,30 @@
+Module Foo.
+  Definition binary A := A -> A -> Prop.
+
+  Definition inter A (R1 R2 : binary A): binary A :=
+    fun (x y:A) => R1 x y /\ R2 x y.
+End Foo.
+
+Module Simple_sparse_proof.
+  Parameter node : Type.
+  Parameter graph : Type.
+  Parameter has_edge : graph -> node -> node -> Prop.
+  Implicit Types x y z : node.
+  Implicit Types G : graph.
+
+  Parameter mem : forall A, A -> list A -> Prop.
+  Hypothesis mem_nil : forall x, mem node x nil = False.
+
+  Definition notin (l: list node): node -> node -> Prop :=
+    fun x y => ~ mem node x l /\ ~ mem node y l.
+
+  Definition edge_notin G l : node -> node -> Prop :=
+    Foo.inter node (has_edge G) (notin l).
+
+  Hint Unfold Foo.inter notin edge_notin : rel_crush.
+
+  Lemma edge_notin_nil G : forall x y, edge_notin G nil x y <-> has_edge G x y.
+  Proof.
+    intros. autounfold with rel_crush. rewrite !mem_nil. tauto.
+  Qed.
+End Simple_sparse_proof.