1 files changed, 28 insertions, 21 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3e6c4858e0..d995786d97 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -21,6 +21,7 @@ let safe_flags oracle = {
   check_guarded = true;
   check_universes = true;
   conv_oracle = oracle;
+  share_reduction = true;
 }
 
 (** {6 Arities } *)
@@ -83,11 +84,6 @@ let subst_const_def sub def = match def with
   | Def c -> Def (subst_constr sub c)
   | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
 
-let subst_const_proj sub pb =
-  { pb with proj_ind = subst_ind sub pb.proj_ind;
-    proj_type = subst_mps sub pb.proj_type;
-  }
-
 let subst_const_body sub cb =
   assert (List.is_empty cb.const_hyps); (* we're outside sections *)
   if is_empty_subst sub then cb
@@ -185,7 +181,7 @@ let subst_regular_ind_arity sub s =
     if uar' == s.mind_user_arity then s 
     else { mind_user_arity = uar'; mind_sort = s.mind_sort }
 
-let subst_template_ind_arity sub s = s
+let subst_template_ind_arity _sub s = s
 
 (* FIXME records *)
 let subst_ind_arity =
@@ -213,10 +209,9 @@ let subst_mind_record sub r = match r with
 | FakeRecord -> FakeRecord
 | PrimRecord infos ->
   let map (id, ps, pb as info) =
-    let ps' = Array.Smart.map (subst_constant sub) ps in
-    let pb' = Array.Smart.map (subst_const_proj sub) pb in
-    if ps' == ps && pb' == pb then info
-    else (id, ps', pb')
+    let pb' = Array.Smart.map (subst_mps sub) pb in
+    if pb' == pb then info
+    else (id, ps, pb')
   in
   let infos' = Array.Smart.map map infos in
   if infos' == infos then r else PrimRecord infos'
@@ -245,14 +240,33 @@ let inductive_polymorphic_context mib =
 let inductive_is_polymorphic mib =
   match mib.mind_universes with
   | Monomorphic_ind _ -> false
-  | Polymorphic_ind ctx -> true
-  | Cumulative_ind cumi -> true
+  | Polymorphic_ind _ctx -> true
+  | Cumulative_ind _cumi -> true
 
 let inductive_is_cumulative mib =
   match mib.mind_universes with
   | Monomorphic_ind _ -> false
-  | Polymorphic_ind ctx -> false
-  | Cumulative_ind cumi -> true
+  | Polymorphic_ind _ctx -> false
+  | Cumulative_ind _cumi -> true
+
+let inductive_make_projection ind mib ~proj_arg =
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> None
+  | PrimRecord infos ->
+    Some (Names.Projection.Repr.make ind
+            ~proj_npars:mib.mind_nparams
+            ~proj_arg
+            (pi2 infos.(snd ind)).(proj_arg))
+
+let inductive_make_projections ind mib =
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> None
+  | PrimRecord infos ->
+    let projs = Array.mapi (fun proj_arg lab ->
+        Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab)
+        (pi2 infos.(snd ind))
+    in
+    Some projs
 
 (** {6 Hash-consing of inductive declarations } *)
 
@@ -292,13 +306,6 @@ let hcons_mind mib =
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_universes = hcons_mind_universes mib.mind_universes }
 
-(** {6 Stm machinery } *)
-
-let string_of_side_effect { Entries.eff } = match eff with
-  | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")"
-  | Entries.SEscheme (cl,_) ->
-      "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")"
-
 (** Hashconsing of modules *)
 
 let hcons_functorize hty he hself f = match f with