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, 16 insertions, 5 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index f269e165e..9c7344f89 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -172,7 +172,9 @@ type mutual_inductive_body = {
 
     mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
 
-  }
+    mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
+  
+}
 
 (** {6 Module declarations } *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 92a566b7c..8806bba45 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -227,7 +227,8 @@ let subst_mind_body sub mib =
       Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_polymorphic = mib.mind_polymorphic;
-    mind_universes = mib.mind_universes }
+    mind_universes = mib.mind_universes;
+    mind_private = mib.mind_private }
 
 (** {6 Hash-consing of inductive declarations } *)
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 1bc3bbd15..a161a6fcb 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -46,7 +46,8 @@ type mutual_inductive_entry = {
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_polymorphic : bool;
-  mind_entry_universes : Univ.universe_context }
+  mind_entry_universes : Univ.universe_context;
+  mind_entry_private : bool option }
 
 (** {6 Constants (Definition/Axiom) } *)
 type proof_output = constr * Declareops.side_effects
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e89bbf0d9..73fdaa81f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -628,6 +628,7 @@ let used_section_variables env inds =
     (fun l c -> Id.Set.union (Environ.global_vars_set env c) l)
       Id.Set.empty inds in
   keep_hyps env ids
+
 let lift_decl n d = 
   map_rel_declaration (lift n) d
 
@@ -660,7 +661,7 @@ let compute_expansion ((kn, _ as ind), u) params ctx =
  	     (Array.map (fun p -> mkProj (p, mkRel 1)) projarr))
    in exp, projarr
 
-let build_inductive env p ctx env_ar params kn isrecord isfinite inds nmr recargs =
+let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps =  used_section_variables env inds in
@@ -743,6 +744,7 @@ let build_inductive env p ctx env_ar params kn isrecord isfinite inds nmr recarg
       mind_packets = packets;
       mind_polymorphic = p;
       mind_universes = ctx;
+      mind_private = prv;
     }
 
 (************************************************************************)
@@ -757,7 +759,7 @@ let check_inductive env kn mie =
   (* Then check positivity conditions *)
   let (nmr,recargs) = check_positivity kn env_ar params inds in
   (* Build the inductive packets *)
-    build_inductive env mie.mind_entry_polymorphic 
+    build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
       env_ar params kn mie.mind_entry_record mie.mind_entry_finite
       inds nmr recargs
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 093ee7024..4c18ed275 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -308,6 +308,11 @@ let rec add_structure mp sign resolver linkinfo env =
       Environ.add_constant_key c cb linkinfo env
     |SFBmind mib ->
       let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in
+      let mib = 
+	if mib.mind_private != None then 
+	  { mib with mind_private = Some true }
+	else mib
+      in
       Environ.add_mind_key mind (mib,linkinfo) env
     |SFBmodule mb -> add_module mb linkinfo env (* adds components as well *)
     |SFBmodtype mtb -> Environ.add_modtype mtb env