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

5 files changed, 14 insertions, 9 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3f2a518886..22830eb6df 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -412,7 +412,7 @@ let inductive_levels env evdref arities inds =
     !evdref (Array.to_list levels') destarities sizes
   in evdref := evd; arities
 
-let interp_mutual_inductive (paramsl,indl) notations poly finite =
+let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   let env0 = Global.env() in
   let evdref = ref Evd.(from_env env0) in
@@ -487,6 +487,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly finite =
     mind_entry_finite = finite;
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
+    mind_entry_private = if prv then Some false else None;
     mind_entry_universes = Evd.universe_context evd },
     impls
 
@@ -535,7 +536,7 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
 		       constrimpls)
       impls;
   if_verbose msg_info (minductive_message names);
-  declare_default_schemes mind;
+  if mie.mind_entry_private == None then declare_default_schemes mind;
   mind
 
 type one_inductive_impls =
@@ -545,10 +546,10 @@ type one_inductive_impls =
 type one_inductive_expr =
   lident * local_binder list * constr_expr option * constructor_expr list
 
-let do_mutual_inductive indl poly finite =
+let do_mutual_inductive indl poly prv finite =
   let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
-  let mie,impls = interp_mutual_inductive indl ntns poly finite in
+  let mie,impls = interp_mutual_inductive indl ntns poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (declare_mutual_inductive_with_eliminations UserVerbose mie impls);
   (* Declare the possible notations of inductive types *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d2e601edd5..41cb5baa3b 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -86,7 +86,8 @@ type one_inductive_impls =
   Impargs.manual_implicits list (** for constrs *)
 
 val interp_mutual_inductive :
-  structured_inductive_expr -> decl_notation list -> polymorphic -> bool(*finite*) ->
+  structured_inductive_expr -> decl_notation list -> polymorphic ->
+    private_flag -> bool(*finite*) ->
     mutual_inductive_entry * one_inductive_impls list
 
 (** Registering a mutual inductive definition together with its
@@ -99,7 +100,8 @@ val declare_mutual_inductive_with_eliminations :
 (** Entry points for the vernacular commands Inductive and CoInductive *)
 
 val do_mutual_inductive :
-  (one_inductive_expr * decl_notation list) list -> polymorphic -> bool -> unit
+  (one_inductive_expr * decl_notation list) list -> polymorphic -> 
+  private_flag -> bool -> unit
 
 (** {6 Fixpoints and cofixpoints} *)
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index e17038a4fe..5d0bcd78b6 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -102,5 +102,6 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_params = params';
     mind_entry_inds = inds';
     mind_entry_polymorphic = mib.mind_polymorphic;
+    mind_entry_private = mib.mind_private;
     mind_entry_universes = univs
   }
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b144dfe43c..56493bae81 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -340,6 +340,7 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f
       mind_entry_finite = finite != CoFinite;
       mind_entry_inds = [mie_ind];
       mind_entry_polymorphic = poly;
+      mind_entry_private = None;
       mind_entry_universes = ctx } in
   let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index bb702f79f7..ca31d1f2ed 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -534,7 +534,7 @@ let vernac_record k poly finite infer struc binders sort nameopt cfs =
 	| _ -> ()) cfs);
     ignore(Record.definition_structure (k,poly,finite,infer,struc,binders,cfs,const,sort))
 
-let vernac_inductive poly finite infer indl =
+let vernac_inductive poly lo finite infer indl =
   if Dumpglob.dump () then
     List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
       match cstrs with
@@ -565,7 +565,7 @@ let vernac_inductive poly finite infer indl =
       | _ -> Errors.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
-    do_mutual_inductive indl poly (finite != CoFinite)
+    do_mutual_inductive indl poly lo (finite != CoFinite)
 
 let vernac_fixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
@@ -1696,7 +1696,7 @@ let interp ?proof locality poly c =
   | VernacEndProof e -> vernac_end_proof ?proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
-  | VernacInductive (finite,infer,l) -> vernac_inductive poly finite infer l
+  | VernacInductive (priv,finite,infer,l) -> vernac_inductive poly priv finite infer l
   | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
   | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
   | VernacScheme l -> vernac_scheme l