Major refactoring of cooking.ml

checker/check.ml

@@ -108,7 +108,7 @@ let indirect_accessor o =
   | None ->  CErrors.user_err Pp.(str "Cannot access opaque delayed proof.")
   | Some c -> c
   in
-  let (c, prv) = Cooking.cook_constr ci c in
+  let (c, prv) = Discharge.cook_opaque_proofterm ci c in
   let c = Mod_subst.(List.fold_right subst_mps sub c) in
   (c, prv)
 

checker/mod_checking.ml

@@ -8,7 +8,7 @@ open Environ
 
 (** {6 Checking constants } *)
 
-let indirect_accessor : (cooking_info Opaqueproof.opaque -> Constr.t * unit Opaqueproof.delayed_universes) ref =
+let indirect_accessor : (Opaqueproof.opaque -> Constr.t * unit Opaqueproof.delayed_universes) ref =
   ref (fun _ -> assert false)
 
 let set_indirect_accessor f = indirect_accessor := f
@@ -55,7 +55,7 @@ let check_constant_declaration env opac kn cb opacify =
       let c, u = !indirect_accessor o in
       let env = match u, cb.const_universes with
         | Opaqueproof.PrivateMonomorphic (), Monomorphic -> env
-        | Opaqueproof.PrivatePolymorphic (_, local), Polymorphic _ ->
+        | Opaqueproof.PrivatePolymorphic local, Polymorphic _ ->
           push_subgraph local env
         | _ -> assert false
       in

checker/mod_checking.mli

@@ -8,6 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val set_indirect_accessor : (Declarations.cooking_info Opaqueproof.opaque -> Constr.t * unit Opaqueproof.delayed_universes) -> unit
+val set_indirect_accessor : (Opaqueproof.opaque -> Constr.t * unit Opaqueproof.delayed_universes) -> unit
 
 val check_module : Environ.env -> Names.Cset.t Names.Cmap.t -> Names.ModPath.t -> Declarations.module_body -> Names.Cset.t Names.Cmap.t

checker/values.ml

@@ -193,21 +193,17 @@ let v_subst =
 
 (** kernel/lazyconstr *)
 
-let v_ndecl = v_sum "named_declaration" 0
-    [| [|v_binder_annot v_id; v_constr|];               (* LocalAssum *)
-       [|v_binder_annot v_id; v_constr; v_constr|] |]   (* LocalDef *)
+let v_abstr_info =
+  Tuple ("abstr_info", [|v_rctxt; v_abs_context; List v_id; v_hmap v_level v_level|])
 
-let v_nctxt = List v_ndecl
+let v_abstr_inst_info =
+  Tuple ("abstr_inst_info", [|List v_id; v_instance|])
 
-let v_work_list =
-  let v_abstr = v_pair v_instance (Array v_id) in
-  Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|])
-
-let v_abstract =
-  Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |])
+let v_expand_info =
+  Tuple ("expand_info", [|v_hmap v_cst v_abstr_inst_info; v_hmap v_cst v_abstr_inst_info|])
 
 let v_cooking_info =
-  Tuple ("cooking_info", [|v_work_list; v_abstract|])
+  Tuple ("cooking_info", [|v_expand_info; v_abstr_info; v_abstr_inst_info; v_set v_id|])
 
 let v_opaque =
   v_sum "opaque" 0 [|[|List v_subst; List v_cooking_info; v_dp; Int|]|]
@@ -431,7 +427,7 @@ let v_lib =
   Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
 
 let v_delayed_universes =
-  Sum ("delayed_universes", 0, [| [| v_unit |]; [| Int; v_context_set |] |])
+  Sum ("delayed_universes", 0, [| [| v_unit |]; [| v_context_set |] |])
 
 let v_opaquetable = Array (Opt (v_pair v_constr v_delayed_universes))
 let v_univopaques =

dev/ci/user-overlays/14727-herbelin-master+major-refactoring-cooking.sh

@@ -0,0 +1,2 @@
+overlay elpi https://github.com/herbelin/coq-elpi coq-master+adapt-coq-pr14727-reworking-cooking 14727
+overlay metacoq https://github.com/herbelin/template-coq.git master+adapt-coq-pr14727-reworking-cooking 14727

interp/impargs.ml

@@ -541,15 +541,14 @@ let subst_implicits (subst,(req,l)) =
 let sec_implicits =
   Summary.ref Id.Map.empty ~name:"section-implicits"
 
-let impls_of_context ctx =
-  let map n decl =
-    let id = NamedDecl.get_id decl in
+let impls_of_context vars =
+  let map n id =
     match Id.Map.get id !sec_implicits with
     | NonMaxImplicit -> Some ((Name id,n,None), Manual, (false, true))
     | MaxImplicit -> Some ((Name id,n,None), Manual, (true, true))
     | Explicit -> None
   in
-  List.map_i map 1 (List.rev (List.filter (NamedDecl.is_local_assum) ctx))
+  List.map_i map 1 vars
 
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
@@ -578,7 +577,7 @@ let discharge_implicits (req,l) =
      let l' =
        try
          List.map (fun (gr, l) ->
-             let vars = Lib.variable_section_segment_of_reference gr in
+             let vars = Array.map_to_list Constr.destVar (Lib.section_instance gr) in
              let extra_impls = impls_of_context vars in
              let newimpls = List.map (add_section_impls vars extra_impls) l in
              (gr, newimpls)) l

interp/notation.ml

@@ -20,7 +20,6 @@ open Constrexpr
 open Notation_term
 open Glob_term
 open Glob_ops
-open Context.Named.Declaration
 open NumTok
 
 (*i*)
@@ -2047,8 +2046,7 @@ let discharge_arguments_scope (req,r,n,l,_) =
   else
     let n =
       try
-        let vars = Lib.variable_section_segment_of_reference r in
-        vars |> List.filter is_local_assum |> List.length
+        Array.length (Lib.section_instance r)
       with
         Not_found (* Not a ref defined in this section *) -> 0 in
     Some (req,r,n,l,[])