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

4 files changed, 28 insertions, 8 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b56d5947ce..2b0a2dda95 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1298,6 +1298,7 @@ and match_current pb (initial,tomatch) =
 	compile_all_variables initial tomatch pb
     | IsInd (_,(IndType(indf,realargs) as indt),names) ->
 	let mind,_ = dest_ind_family indf in
+        let mind = Tacred.check_privacy pb.env mind in
 	let cstrs = get_constructors pb.env indf in
 	let arsign, _ = get_arity pb.env indf in
 	let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 35a9cbdb22..bed77e6223 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -45,6 +45,15 @@ let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c)
 (* Building curryfied elimination          *)
 (*******************************************)
 
+let is_private mib =
+  match mib.mind_private with
+  | Some true -> true
+  | _ -> false
+
+let check_privacy_block mib =
+  if is_private mib then
+    errorlabstrm ""(str"case analysis on a private inductive type")
+      
 (**********************************************************************)
 (* Building case analysis schemes *)
 (* Christine Paulin, 1996 *)
@@ -54,12 +63,13 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
   let lnamespar = Vars.subst_univs_context usubst
     mib.mind_params_ctxt
   in
-
-  if not (Sorts.List.mem kind (elim_sorts specif)) then
-    raise
-      (RecursionSchemeError
-	 (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind)));
-
+  let () = check_privacy_block mib in
+  let () = 
+    if not (Sorts.List.mem kind (elim_sorts specif)) then
+      raise
+	(RecursionSchemeError
+	   (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind)))
+  in
   let ndepar = mip.mind_nrealargs_ctxt + 1 in
 
   (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index da45952548..383d233069 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1093,6 +1093,10 @@ let pattern_occs loccs_trm env sigma c =
 
 (* Used in several tactics. *)
 
+let check_privacy env ind =
+  if (fst (Inductive.lookup_mind_specif env (fst ind))).Declarations.mind_private = Some true then
+    errorlabstrm "" (str "case analysis on a private type")
+  else ind
 (* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
    return name, B and t' *)
 
@@ -1100,7 +1104,7 @@ let reduce_to_ind_gen allow_product env sigma t =
   let rec elimrec env t l =
     let t = hnf_constr env sigma t in
     match kind_of_term (fst (decompose_app t)) with
-      | Ind ind-> (ind, it_mkProd_or_LetIn t l)
+      | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l)
       | Prod (n,ty,t') ->
 	  if allow_product then
 	    elimrec (push_rel (n,None,ty) env) t' ((n,None,ty)::l)
@@ -1111,7 +1115,7 @@ let reduce_to_ind_gen allow_product env sigma t =
 	     was partially the case between V5.10 and V8.1 *)
 	  let t' = whd_betadeltaiota env sigma t in
 	  match kind_of_term (fst (decompose_app t')) with
-	    | Ind ind-> (ind, it_mkProd_or_LetIn t' l)
+	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
 	    | _ -> errorlabstrm "" (str"Not an inductive product.")
   in
   elimrec env t []
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 5146cd3458..5e4bc5c461 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -14,6 +14,7 @@ open Reductionops
 open Pattern
 open Globnames
 open Locus
+open Univ
 
 type reduction_tactic_error =
     InvalidAbstraction of env * constr * (env * Type_errors.type_error)
@@ -106,3 +107,7 @@ val contextually : bool -> occurrences * constr_pattern ->
 
 val e_contextually : bool -> occurrences * constr_pattern ->
   (patvar_map -> e_reduction_function) -> e_reduction_function
+
+(** Returns the same inductive if it is allowed for pattern-matching
+    raises an error otherwise. **)
+val check_privacy : env -> inductive puniverses -> inductive puniverses