Give a way to control if the decidable-equality schemes are built like

in 8.4 with the schemes of the subcomponent of an inductive added to
the environment or discharged as let-ins over the main scheme.

As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).

1 files changed, 15 insertions, 17 deletions

diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 0d39466ed..b59d6fc8a 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -28,11 +28,10 @@ open Pp
 (**********************************************************************)
 (* Registering schemes in the environment *)
 
-
 type mutual_scheme_object_function =
-  mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
 type individual_scheme_object_function =
-  inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
 
 type 'a scheme_kind = string
 
@@ -141,32 +140,31 @@ let define internal id c p univs =
   in
   kn
 
-let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
-  let (c, ctx), eff = f ind in
+let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
+  let (c, ctx), eff = f mode ind in
   let mib = Global.lookup_mind mind in
   let id = match idopt with
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
-  let const = define internal id c mib.mind_polymorphic ctx in
+  let const = define mode id c mib.mind_polymorphic ctx in
   declare_scheme kind [|ind,const|];
   const, Declareops.cons_side_effects
      (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff
 
-let define_individual_scheme kind internal names (mind,i as ind) =
+let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
   | _,MutualSchemeFunction f -> assert false
   | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f internal names ind
+      define_individual_scheme_base kind s f mode names ind
 
-let define_mutual_scheme_base kind suff f internal names mind =
-  let (cl, ctx), eff = f mind in
+let define_mutual_scheme_base kind suff f mode names mind =
+  let (cl, ctx), eff = f mode mind in
   let mib = Global.lookup_mind mind in
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
       try Int.List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
-
   let consts = Array.map2 (fun id cl -> 
-     define internal id cl mib.mind_polymorphic ctx) ids cl in
+     define mode id cl mib.mind_polymorphic ctx) ids cl in
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
   consts,
@@ -175,11 +173,11 @@ let define_mutual_scheme_base kind suff f internal names mind =
       kind (Global.safe_env()) (Array.to_list schemes))
     eff 
 
-let define_mutual_scheme kind internal names mind =
+let define_mutual_scheme kind mode names mind =
   match Hashtbl.find scheme_object_table kind with
   | _,IndividualSchemeFunction _ -> assert false
   | s,MutualSchemeFunction f ->
-      define_mutual_scheme_base kind s f internal names mind
+      define_mutual_scheme_base kind s f mode names mind
 
 let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
@@ -188,14 +186,14 @@ let find_scheme_on_env_too kind ind =
             kind (Global.safe_env()) [ind, s])
       Declareops.no_seff 
 
-let find_scheme kind (mind,i as ind) =
+let find_scheme ?(mode=KernelSilent) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
   | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f KernelSilent None ind
+      define_individual_scheme_base kind s f mode None ind
   | s,MutualSchemeFunction f ->
-      let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in
+      let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
       ca.(i), eff
 
 let check_scheme kind ind =