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 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'tactics')

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;
-- 
cgit v1.2.3