From 8a905458039b631165d068bbf62f88e11eb36eb1 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Sat, 2 Mar 2013 14:00:46 -0500
Subject: 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
---
 kernel/modops.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 093ee70247..4c18ed2752 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
-- 
cgit v1.2.3