[equations] [proof] Remove duplicate shrink function.

Equation's terminator had exactly duplicated the shrink function used
in `Abstract`, we remove this duplicity.

3 files changed, 33 insertions, 75 deletions

diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index 9d4f3cfb27..0c74e898d2 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -20,3 +20,11 @@ val cache_term_by_tactic_then
   -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+
+(* Internal but used in a few places; should likely be made intro a
+   proper library function, or incorporated into the generic constant
+   save path *)
+val shrink_entry
+  :  ('a, 'b) Context.Named.Declaration.pt list
+  -> 'c Entries.definition_entry
+  -> 'c Entries.definition_entry * Constr.t list
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 71215d2a3e..30aa347692 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -95,6 +95,7 @@ let decompose_lam_prod c ty =
   in
   aux Context.Rel.empty c ty
 
+(* XXX: What's the relation of this with Abstract.shrink ? *)
 let shrink_body c ty =
   let ctx, b, ty =
     match ty with
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 091ff32009..a1345f444b 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -581,81 +581,30 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries =
   in
   ignore (Declare.declare_constant name lemma_def)
 
-(* XXX several versions of shrink do appear in abstract, declareobl and here *)
-module Equations = struct
-  let rec decompose len c t accu =
-    let open Constr in
-    let open Context.Rel.Declaration in
-    if len = 0 then (c, t, accu)
-    else match kind c, kind t with
-      | Lambda (na, u, c), Prod (_, _, t) ->
-        decompose (pred len) c t (LocalAssum (na, u) :: accu)
-      | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
-        decompose (pred len) c t (LocalDef (na, b, u) :: accu)
-      | _ -> assert false
-
-  let rec shrink ctx sign c t accu =
-    let open Constr in
-    let open Vars in
-    match ctx, sign with
-    | [], [] -> (c, t, accu)
-    | p :: ctx, decl :: sign ->
-      if noccurn 1 c && noccurn 1 t then
-        let c = subst1 mkProp c in
-        let t = subst1 mkProp t in
-        shrink ctx sign c t accu
-      else
-        let c = Term.mkLambda_or_LetIn p c in
-        let t = Term.mkProd_or_LetIn p t in
-        let accu = if RelDecl.is_local_assum p
-          then mkVar (NamedDecl.get_id decl) :: accu
-          else accu
-        in
-        shrink ctx sign c t accu
-    | _ -> assert false
+let finish_proved_equations opaque lid proof_obj hook i types wits sigma =
 
-  let shrink_entry sign const =
-    let open Entries in
-    let typ = match const.const_entry_type with
-      | None -> assert false
-      | Some t -> t
-    in
-    (* The body has been forced by the call to [build_constant_by_tactic] *)
-    (* let () = assert (Future.is_over const.const_entry_body) in *)
-    let ((body, uctx), eff) = Future.force const.const_entry_body in
-    let (body, typ, ctx) = decompose (List.length sign) body typ [] in
-    let (body, typ, args) = shrink ctx sign body typ [] in
-    let const = { const with
-                  const_entry_body = Future.from_val ((body, uctx), eff);
-                  const_entry_type = Some typ;
-                } in
-    (const, args)
-
-  let finish_proved opaque lid proof_obj hook i types wits sigma =
-
-    let open Decl_kinds in
-    let obls = ref 1 in
-    let kind = match pi3 proof_obj.Proof_global.persistence with
-      | DefinitionBody d -> IsDefinition d
-      | Proof p -> IsProof p
-    in
-    let evd = ref sigma in
-    let recobls =
-      CList.map2 (fun (wit, (evar_env, ev, evi, local_context, type_)) entry ->
-          let id =
-            match Evd.evar_ident ev sigma with
-            | Some id -> id
-            | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n)
-          in
-          let entry, args = shrink_entry local_context entry in
-          let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in
-          let sigma, app = Evarutil.new_global !evd (ConstRef cst) in
-          evd := Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma;
-          cst)
-        (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries
-    in
-    hook recobls !evd
-end
+  let open Decl_kinds in
+  let obls = ref 1 in
+  let kind = match pi3 proof_obj.Proof_global.persistence with
+    | DefinitionBody d -> IsDefinition d
+    | Proof p -> IsProof p
+  in
+  let evd = ref sigma in
+  let recobls =
+    CList.map2 (fun (wit, (evar_env, ev, evi, local_context, type_)) entry ->
+        let id =
+          match Evd.evar_ident ev sigma with
+          | Some id -> id
+          | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n)
+        in
+        let entry, args = Abstract.shrink_entry local_context entry in
+        let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in
+        let sigma, app = Evarutil.new_global !evd (ConstRef cst) in
+        evd := Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma;
+        cst)
+      (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries
+  in
+  hook recobls !evd
 
 let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
   (* Invariant (uh) *)
@@ -682,4 +631,4 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
   | End_derive { f ; name } ->
     finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries
   | End_equations { hook; i; types; wits; sigma } ->
-    Equations.finish_proved opaque idopt proof_obj hook i types wits sigma
+    finish_proved_equations opaque idopt proof_obj hook i types wits sigma