From 24c570834dccc90c7ff14d3f6b9d33b818fa79c9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Apr 2019 18:50:47 +0200
Subject: Fix #9994: `revert dependent` is extremely slow.

We add a fast path when generalizing over variables.
---
 tactics/tactics.ml                 | 18 +++++++++++-------
 test-suite/bugs/closed/bug_10025.v | 39 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 50 insertions(+), 7 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_10025.v

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 16bede0d1b..35b3b38298 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2863,17 +2863,21 @@ let generalize_dep ?(with_let=false) c =
       | _ -> tothin
   in
   let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
-  let body =
-    if with_let then
-      match EConstr.kind sigma c with
-      | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value
-      | _ -> None
-    else None
+  let is_var, body = match EConstr.kind sigma c with
+  | Var id ->
+    let body = NamedDecl.get_value (pf_get_hyp id gl) in
+    let is_var = Option.is_empty body && not (List.mem id init_ids) in
+    if with_let then is_var, body else is_var, None
+  | _ -> false, None
   in
   let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
     (cl',project gl) in
   (* Check that the generalization is indeed well-typed *)
-  let (evd, _) = Typing.type_of env evd cl'' in
+  let evd =
+    (* No need to retype for variables, term is statically well-typed *)
+    if is_var then evd
+    else fst (Typing.type_of env evd cl'')
+  in
   let args = Context.Named.to_instance mkVar to_quantify_rev in
   tclTHENLIST
     [ Proofview.Unsafe.tclEVARS evd;
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.
-- 
cgit v1.2.3