From 30ed0b3385d80e2abe3d2d8c67ce09643a8bf74c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 29 May 2019 16:35:51 +0200
Subject: Fix #10268: vio2vo produces incorrect term when discharging.

We do not partially abstract the section info. Instead, we reuse the same
code in cook_constr and cook_constant and pass the same section info.
---
 kernel/cooking.ml        | 36 ++++++++++++++++++------------------
 test-suite/vio/section.v | 12 ++++++++++++
 2 files changed, 30 insertions(+), 18 deletions(-)
 create mode 100644 test-suite/vio/section.v

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index c08b537697..620efbafd6 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -165,26 +165,11 @@ type 'opaque result = {
   cook_context : Constr.named_context option;
 }
 
-let on_body ml hy f = function
-  | Undef _ as x -> x
-  | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs)))
-  | OpaqueDef o ->
-    OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
-                 { Opaqueproof.modlist = ml; abstract = hy } o)
-  | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
-
 let expmod_constr_subst cache modlist subst c =
   let subst = Univ.make_instance_subst subst in
   let c = expmod_constr cache modlist c in
     Vars.subst_univs_level_constr subst c
 
-let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
-  let cache = RefTable.create 13 in
-  let expmod = expmod_constr_subst cache modlist subst in
-  let hyps = Context.Named.map expmod vars in
-  let hyps = abstract_context hyps in
-  abstract_constant_body (expmod c) hyps
-
 let discharge_abstract_universe_context subst abs_ctx auctx =
   (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract
       context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
@@ -217,6 +202,18 @@ let lift_univs cb subst auctx0 =
     let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in
     subst, (Polymorphic auctx)
 
+let cook_constr { Opaqueproof.modlist ; abstract } c =
+  let cache = RefTable.create 13 in
+  let abstract, usubst, abs_ctx = abstract in
+  (* For now the STM only handles deferred computation of monomorphic
+    constants. The API will need to be adapted when it's not the case
+    anymore. *)
+  let () = assert (AUContext.is_empty abs_ctx) in
+  let expmod = expmod_constr_subst cache modlist usubst in
+  let hyps = Context.Named.map expmod abstract in
+  let hyps = abstract_context hyps in
+  abstract_constant_body (expmod c) hyps
+
 let cook_constant { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
   let cache = RefTable.create 13 in
@@ -226,9 +223,12 @@ let cook_constant { from = cb; info } =
   let hyps0 = Context.Named.map expmod abstract in
   let hyps = abstract_context hyps0 in
   let map c = abstract_constant_body (expmod c) hyps in
-  let body = on_body modlist (hyps0, usubst, abs_ctx)
-    map
-    cb.const_body
+  let body = match cb.const_body with
+  | Undef _ as x -> x
+  | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
+  | OpaqueDef o ->
+    OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:map info o)
+  | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
   let const_hyps =
     Context.Named.fold_outside (fun decl hyps ->
diff --git a/test-suite/vio/section.v b/test-suite/vio/section.v
new file mode 100644
index 0000000000..0e7722516a
--- /dev/null
+++ b/test-suite/vio/section.v
@@ -0,0 +1,12 @@
+Section Foo.
+  Variable A : Type.
+
+  Definition bla := A.
+
+  Variable B : bla.
+
+  Lemma blu : {X:Type & X}.
+  Proof using A B.
+    exists bla;exact B.
+  Qed.
+End Foo.
-- 
cgit v1.2.3