Fix #9994: `revert dependent` is extremely slow.

We add a fast path when generalizing over variables.

1 files changed, 39 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_10025.v b/test-suite/bugs/closed/bug_10025.v
new file mode 100644
index 0000000000..1effc771b0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10025.v
@@ -0,0 +1,39 @@
+Require Import Program.
+
+Axiom I : Type.
+
+Inductive S : Type := NT : I -> S.
+
+Axiom F : S -> Type.
+
+Axiom G : forall (s : S), F s -> Type.
+
+Section S.
+
+Variable init : I.
+Variable my_s : F (NT init).
+
+Inductive foo : forall (s: S) (hole_sem: F s), Type :=
+| Foo : foo (NT init) my_s.
+
+Goal forall
+  (n : I) (s : F (NT n)) (ptz : foo (NT n) s) (pt : G (NT n) s) (x : unit),
+match
+  match x with tt => tt end
+with
+| tt =>
+    match
+      match ptz in foo x s return (forall _ : G x s, unit) with
+      | Foo => fun _ : G (NT init) my_s => tt
+      end pt
+    with
+    | tt => False
+    end
+end.
+Proof.
+dependent destruction ptz.
+(* Check well-typedness of goal *)
+match goal with [ |- ?P ] => let t := type of P in idtac end.
+Abort.
+
+End S.