Adapt Y. Bertot's path on private inductives (now the keyword is "Private").

A quick and dirty approach to private inductive types
Types for which computable functions are provided, but pattern-matching is disallowed.
This kind of type can be used to simulate simple forms of higher inductive types, with
convertibility for applications of the inductive principle to 0-constructors

Conflicts:
	intf/vernacexpr.mli
	kernel/declarations.ml
	kernel/declarations.mli
	kernel/entries.mli
	kernel/indtypes.ml
	library/declare.ml
	parsing/g_vernac.ml4
	plugins/funind/glob_term_to_relation.ml
	pretyping/indrec.ml
	pretyping/tacred.mli
	printing/ppvernac.ml
	toplevel/vernacentries.ml

Conflicts:
	kernel/declarations.mli
	kernel/declareops.ml
	kernel/indtypes.ml
	kernel/modops.ml

1 files changed, 2 insertions, 1 deletions

diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 2e524a35f0..6eabe6e871 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -884,7 +884,8 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
-  let mie,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) true (* means: not coinductive *) in
+  let mie,impls = Command.interp_mutual_inductive indl [] 
+          false (*FIXMEnon-poly *) false (* means not private *) true (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)