Merge remote-tracking branch 'origin/master' into stm+doc_hook

7 files changed, 68 insertions, 83 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e5bf52571c..bb66658a37 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -850,10 +850,10 @@ let rec extern inctx scopes vars r =
 		     | Some c :: q ->
 		         match locs with
 			   | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
-			   | (_, false) :: locs' ->
+                           | { Recordops.pk_true_proj = false } :: locs' ->
 			       (* we don't want to print locals *)
 			       ip q locs' args acc
-			   | (_, true) :: locs' ->
+                           | { Recordops.pk_true_proj = true } :: locs' ->
 			       match args with
 				 | [] -> raise No_match
 				     (* we give up since the constructor is not complete *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c0801067ce..f06493b374 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1368,7 +1368,7 @@ let sort_fields ~complete loc fields completer =
                  let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
                  begin match proj_kinds with
                     | [] -> anomaly (Pp.str "Number of projections mismatch.")
-                    | (_, regular) :: proj_kinds ->
+                    | { Recordops.pk_true_proj = regular } :: proj_kinds ->
                        (* "regular" is false when the field is defined
                            by a let-in in the record declaration
                            (its value is fixed from other fields). *)
diff --git a/interp/declare.ml b/interp/declare.ml
index 76b4bab2ce..7ee7ecb5e8 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -36,9 +36,8 @@ type internal_flag =
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
-  cst_decl : global_declaration option;
-  (** [None] when the declaration is a side-effect and has already been defined
-      in the global environment. *)
+  cst_decl : Cooking.recipe option;
+  (** Non-empty only when rebuilding a constant after a section *)
   cst_kind : logical_kind;
   cst_locl : bool;
 }
@@ -65,21 +64,21 @@ let open_constant i ((sp,kn), obj) =
 let exists_name id =
   variable_exists id || Global.exists_objlabel (Label.of_id id)
 
-let check_exists sp =
-  let id = basename sp in
+let check_exists id =
   if exists_name id then alreadydeclared (Id.print id ++ str " already exists")
 
 let cache_constant ((sp,kn), obj) =
+  (* Invariant: the constant must exist in the logical environment, except when
+     redefining it when exiting a section. See [discharge_constant]. *)
   let id = basename sp in
   let kn' =
     match obj.cst_decl with
     | None ->
       if Global.exists_objlabel (Label.of_id (basename sp))
       then Constant.make1 kn
-      else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
-    | Some decl ->
-      let () = check_exists sp in
-      Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl
+      else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".")
+    | Some r ->
+      Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r
   in
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
@@ -93,7 +92,9 @@ let discharge_constant ((sp, kn), obj) =
   let modlist = replacement_context () in
   let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in
   let abstract = (named_of_variable_context hyps, subst, uctx) in
-  let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
+  let new_decl = { from; info = { Opaqueproof.modlist; abstract } } in
+  (* This is a hack: when leaving a section, we lose the constant definition, so
+     we have to store it in the libobject to be able to retrieve it after. *)
   Some { obj with cst_decl = Some new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -121,27 +122,22 @@ let update_tables c =
   declare_constant_implicits c;
   Notation.declare_ref_arguments_scope Evd.empty (ConstRef c)
 
-let register_side_effect (c, role) =
+let register_constant kn kind local =
   let o = inConstant {
     cst_decl = None;
-    cst_kind = IsProof Theorem;
-    cst_locl = false;
+    cst_kind = kind;
+    cst_locl = local;
   } in
-  let id = Label.to_id (Constant.label c) in
-  ignore(add_leaf id o);
-  update_tables c;
+  let id = Label.to_id (Constant.label kn) in
+  let _ = add_leaf id o in
+  update_tables kn
+
+let register_side_effect (c, role) =
+  let () = register_constant c (IsProof Theorem) false in
   match role with
   | Subproof -> ()
   | Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
 
-let declare_constant_common id cst =
-  let o = inConstant cst in
-  let _, kn as oname = add_leaf id o in
-  pull_to_head oname;
-  let c = Global.constant_of_delta_kn kn in
-  update_tables c;
-  c
-
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
@@ -153,7 +149,8 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let define_constant ?role ?(export_seff=false) id cd =
+  (* Logically define the constant and its subproofs, no libobject tampering *)
   let is_poly de = match de.const_entry_universes with
   | Monomorphic_entry _ -> false
   | Polymorphic_entry _ -> true
@@ -165,20 +162,27 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
         export_seff ||
         not de.const_entry_opaque ||
         is_poly de ->
-      (* This globally defines the side-effects in the environment. We mark
-         exported constants as being side-effect not to redeclare them at
-         caching time. *)
+      (* This globally defines the side-effects in the environment. *)
       let de, export = Global.export_private_constants ~in_section de in
       export, ConstantEntry (PureEntry, DefinitionEntry de)
     | _ -> [], ConstantEntry (EffectEntry, cd)
   in
+  let kn, eff = Global.add_constant ?role ~in_section id decl in
+  kn, eff, export
+
+let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+  let () = check_exists id in
+  let kn, _eff, export = define_constant ~export_seff id cd in
+  (* Register the libobjects attached to the constants and its subproofs *)
   let () = List.iter register_side_effect export in
-  let cst = {
-    cst_decl = Some decl;
-    cst_kind = kind;
-    cst_locl = local;
-  } in
-  declare_constant_common id cst
+  let () = register_constant kn kind local in
+  kn
+
+let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = false) id (cd, kind) =
+  let kn, eff, export = define_constant ~role id cd in
+  let () = assert (List.is_empty export) in
+  let () = register_constant kn kind local in
+  kn, eff
 
 let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
@@ -297,7 +301,7 @@ let open_inductive i ((sp,kn),mie) =
 
 let cache_inductive ((sp,kn),mie) =
   let names = inductive_names sp kn mie in
-  List.iter check_exists (List.map fst names);
+  List.iter check_exists (List.map (fun p -> basename (fst p)) names);
   let id = basename sp in
   let kn' = Global.add_mind id mie in
   assert (MutInd.equal kn' (MutInd.make1 kn));
diff --git a/interp/declare.mli b/interp/declare.mli
index 8f1e73c88c..2ffde31fc0 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -55,6 +55,9 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
 val declare_constant :
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
 
+val declare_private_constant :
+  role:side_effect_role -> ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants
+
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> Id.t -> ?types:constr ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d83a0ce918..806fe93297 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -120,8 +120,6 @@ let argument_position_eq p1 p2 = match p1, p2 with
 | Hyp h1, Hyp h2 -> Int.equal h1 h2
 | _ -> false
 
-let explicitation_eq = Constrexpr_ops.explicitation_eq
-
 type implicit_explanation =
   | DepRigid of argument_position
   | DepFlex of argument_position
@@ -499,9 +497,9 @@ type implicit_interactive_request =
 
 type implicit_discharge_request =
   | ImplLocal
-  | ImplConstant of Constant.t * implicits_flags
+  | ImplConstant of implicits_flags
   | ImplMutualInductive of MutInd.t * implicits_flags
-  | ImplInteractive of GlobRef.t * implicits_flags *
+  | ImplInteractive of implicits_flags *
       implicit_interactive_request
 
 let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits"
@@ -554,39 +552,24 @@ let add_section_impls vars extra_impls (cond,impls) =
 let discharge_implicits (_,(req,l)) =
   match req with
   | ImplLocal -> None
-  | ImplInteractive (ref,flags,exp) ->
-    (try
-      let vars = variable_section_segment_of_reference ref in
-      let extra_impls = impls_of_context vars in
-      let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
-      Some (ImplInteractive (ref,flags,exp),l')
-    with Not_found -> (* ref not defined in this section *) Some (req,l))
-  | ImplConstant (con,flags) ->
-    (try
-      let vars = variable_section_segment_of_reference (ConstRef con) in
-      let extra_impls = impls_of_context vars in
-      let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
-      let l' = [ConstRef con,newimpls] in
-        Some (ImplConstant (con,flags),l')
-    with Not_found -> (* con not defined in this section *) Some (req,l))
-  | ImplMutualInductive (kn,flags) ->
-    (try
-      let l' = List.map (fun (gr, l) ->
-	let vars = variable_section_segment_of_reference gr in
-	let extra_impls = impls_of_context vars in
-        (gr,
-	 List.map (add_section_impls vars extra_impls) l)) l
-      in
-        Some (ImplMutualInductive (kn,flags),l')
-    with Not_found -> (* ref not defined in this section *) Some (req,l))
+  | ImplMutualInductive _ | ImplInteractive _ | ImplConstant _ ->
+     let l' =
+       try
+         List.map (fun (gr, l) ->
+             let vars = variable_section_segment_of_reference 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
+       with Not_found -> l in
+     Some (req,l')
 
 let rebuild_implicits (req,l) =
   match req with
   | ImplLocal -> assert false
-  | ImplConstant (con,flags) ->
-      let oldimpls = snd (List.hd l) in
-      let newimpls = compute_constant_implicits flags con in
-      req, [ConstRef con, List.map2 merge_impls oldimpls newimpls]
+  | ImplConstant flags ->
+      let ref,oldimpls = List.hd l in
+      let newimpls = compute_global_implicits flags ref in
+      req, [ref, List.map2 merge_impls oldimpls newimpls]
   | ImplMutualInductive (kn,flags) ->
       let newimpls = compute_all_mib_implicits flags kn in
       let rec aux olds news =
@@ -597,15 +580,14 @@ let rebuild_implicits (req,l) =
        | _, _ -> assert false
       in req, aux l newimpls
 
-  | ImplInteractive (ref,flags,o) ->
+  | ImplInteractive (flags,o) ->
+      let ref,oldimpls = List.hd l in
       (if isVarRef ref && is_in_section ref then ImplLocal else req),
       match o with
       | ImplAuto ->
-         let oldimpls = snd (List.hd l) in
          let newimpls = compute_global_implicits flags ref in
          [ref,List.map2 merge_impls oldimpls newimpls]
       | ImplManual userimplsize ->
-         let oldimpls = snd (List.hd l) in
          if flags.auto then
            let newimpls = List.hd (compute_global_implicits flags ref) in
            let p = List.length (snd newimpls) - userimplsize in
@@ -640,7 +622,7 @@ let declare_implicits_gen req flags ref =
 let declare_implicits local ref =
   let flags = { !implicit_args with auto = true } in
   let req =
-    if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in
+    if is_local local ref then ImplLocal else ImplInteractive(flags,ImplAuto) in
     declare_implicits_gen req flags ref
 
 let declare_var_implicits id =
@@ -649,7 +631,7 @@ let declare_var_implicits id =
 
 let declare_constant_implicits con =
   let flags = !implicit_args in
-    declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con)
+    declare_implicits_gen (ImplConstant flags) flags (ConstRef con)
 
 let declare_mib_implicits kn =
   let flags = !implicit_args in
@@ -699,7 +681,7 @@ let declare_manual_implicits local ref ?enriching l =
   let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in
   let req =
     if is_local local ref then ImplLocal
-    else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
+    else ImplInteractive(flags,ImplManual (List.length autoimpls))
   in add_anonymous_leaf (inImplicits (req,[ref,l]))
 
 let maybe_declare_manual_implicits local ref ?enriching l =
@@ -758,7 +740,7 @@ let set_implicits local ref l =
             compute_implicit_statuses autoimpls imps)) l in
   let req =
     if is_local local ref then ImplLocal
-    else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
+    else ImplInteractive(flags,ImplManual (List.length autoimpls))
   in add_anonymous_leaf (inImplicits (req,[ref,l']))
 
 let extract_impargs_data impls =
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 0070423530..ccdd448460 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -143,7 +143,3 @@ val projection_implicits : env -> Projection.t -> implicit_status list ->
 val select_impargs_size : int -> implicits_list list -> implicit_status list
 
 val select_stronger_impargs : implicits_list list -> implicit_status list
-
-val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
-  [@@ocaml.deprecated "Use Constrexpr_ops.explicitation_eq instead (since 8.10)"]
-(** Equality on [explicitation]. *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index dffccf02fc..6277d874dd 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -281,7 +281,7 @@ let implicits_of_glob_constr ?(with_products=true) l =
           | _ -> ()
         in []
     | GLambda (na, bk, t, b) -> abs na bk b
-    | GLetIn (na, b, t, c) -> aux i b
+    | GLetIn (na, b, t, c) -> aux i c
     | GRec (fix_kind, nas, args, tys, bds) ->
       let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
       List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)