aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend68
-rwxr-xr-xconfigure4
-rw-r--r--kernel/closure.ml10
-rw-r--r--kernel/closure.mli3
-rw-r--r--kernel/declarations.ml5
-rw-r--r--kernel/declarations.mli4
-rw-r--r--kernel/indtypes.ml4
-rw-r--r--kernel/inductive.ml8
-rw-r--r--kernel/inductive.mli8
-rw-r--r--kernel/mod_typing.ml6
-rw-r--r--kernel/modops.ml53
-rw-r--r--kernel/modops.mli4
-rw-r--r--kernel/reduction.ml11
-rw-r--r--kernel/subtyping.ml63
-rw-r--r--library/declaremods.ml6
-rw-r--r--library/lib.ml6
-rw-r--r--library/lib.mli6
-rwxr-xr-xlibrary/nametab.ml6
-rw-r--r--parsing/prettyp.ml12
-rw-r--r--toplevel/vernacentries.ml22
20 files changed, 217 insertions, 92 deletions
diff --git a/.depend b/.depend
index 1eae2938e..7c790d5fa 100644
--- a/.depend
+++ b/.depend
@@ -215,7 +215,7 @@ tactics/dhyp.cmi: parsing/genarg.cmi kernel/names.cmi proofs/tacexpr.cmo \
tactics/elim.cmi: kernel/names.cmi proofs/proof_type.cmi \
pretyping/rawterm.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
tactics/tacticals.cmi kernel/term.cmi
-tactics/equality.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \
+tactics/equality.cmi: kernel/environ.cmi pretyping/evd.cmi \
tactics/hipattern.cmi kernel/names.cmi pretyping/pattern.cmi \
proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \
@@ -402,10 +402,12 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \
parsing/pptactic.cmx parsing/printer.cmx proofs/proof_trees.cmx \
proofs/refiner.cmx kernel/sign.cmx lib/system.cmx proofs/tacmach.cmx \
kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx kernel/univ.cmx
-kernel/closure.cmo: kernel/environ.cmi kernel/esubst.cmi kernel/names.cmi \
- lib/pp.cmi kernel/term.cmi lib/util.cmi kernel/closure.cmi
-kernel/closure.cmx: kernel/environ.cmx kernel/esubst.cmx kernel/names.cmx \
- lib/pp.cmx kernel/term.cmx lib/util.cmx kernel/closure.cmi
+kernel/closure.cmo: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/esubst.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+ lib/util.cmi kernel/closure.cmi
+kernel/closure.cmx: kernel/declarations.cmx kernel/environ.cmx \
+ kernel/esubst.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+ lib/util.cmx kernel/closure.cmi
kernel/conv_oracle.cmo: kernel/closure.cmi kernel/names.cmi \
kernel/conv_oracle.cmi
kernel/conv_oracle.cmx: kernel/closure.cmx kernel/names.cmx \
@@ -574,12 +576,14 @@ library/declare.cmx: kernel/declarations.cmx kernel/entries.cmx \
kernel/typeops.cmx kernel/univ.cmx lib/util.cmx library/declare.cmi
library/declaremods.cmo: kernel/declarations.cmi kernel/entries.cmi \
library/global.cmi library/lib.cmi library/libnames.cmi \
- library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
- library/summary.cmi lib/util.cmi library/declaremods.cmi
+ library/libobject.cmi kernel/modops.cmi kernel/names.cmi \
+ library/nametab.cmi lib/pp.cmi library/summary.cmi lib/util.cmi \
+ library/declaremods.cmi
library/declaremods.cmx: kernel/declarations.cmx kernel/entries.cmx \
library/global.cmx library/lib.cmx library/libnames.cmx \
- library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
- library/summary.cmx lib/util.cmx library/declaremods.cmi
+ library/libobject.cmx kernel/modops.cmx kernel/names.cmx \
+ library/nametab.cmx lib/pp.cmx library/summary.cmx lib/util.cmx \
+ library/declaremods.cmi
library/global.cmo: kernel/environ.cmi kernel/inductive.cmi \
library/libnames.cmi kernel/names.cmi kernel/safe_typing.cmi \
kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
@@ -1396,32 +1400,30 @@ tactics/eqdecide.cmx: tactics/auto.cmx toplevel/cerrors.cmx \
proofs/proof_type.cmx pretyping/rawterm.cmx proofs/refiner.cmx \
proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
kernel/term.cmx lib/util.cmx
-tactics/equality.cmo: proofs/clenv.cmi parsing/coqast.cmi parsing/coqlib.cmi \
+tactics/equality.cmo: proofs/clenv.cmi parsing/coqlib.cmi \
kernel/declarations.cmi kernel/environ.cmi proofs/evar_refiner.cmi \
- pretyping/evarutil.cmi lib/gmapl.cmi tactics/hipattern.cmi \
- pretyping/indrec.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \
- pretyping/instantiate.cmi library/libobject.cmi proofs/logic.cmi \
- library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
- proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \
- pretyping/retyping.cmi tactics/setoid_replace.cmi tactics/tacinterp.cmi \
- proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \
- tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \
- kernel/typeops.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \
- toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi tactics/wcclausenv.cmi \
- tactics/equality.cmi
-tactics/equality.cmx: proofs/clenv.cmx parsing/coqast.cmx parsing/coqlib.cmx \
+ pretyping/evarutil.cmi tactics/hipattern.cmi pretyping/indrec.cmi \
+ kernel/inductive.cmi pretyping/inductiveops.cmi pretyping/instantiate.cmi \
+ proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
+ pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \
+ pretyping/rawterm.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
+ tactics/setoid_replace.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \
+ pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+ kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi \
+ pretyping/typing.cmi kernel/univ.cmi lib/util.cmi toplevel/vernacexpr.cmo \
+ toplevel/vernacinterp.cmi tactics/wcclausenv.cmi tactics/equality.cmi
+tactics/equality.cmx: proofs/clenv.cmx parsing/coqlib.cmx \
kernel/declarations.cmx kernel/environ.cmx proofs/evar_refiner.cmx \
- pretyping/evarutil.cmx lib/gmapl.cmx tactics/hipattern.cmx \
- pretyping/indrec.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \
- pretyping/instantiate.cmx library/libobject.cmx proofs/logic.cmx \
- library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
- proofs/proof_type.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \
- pretyping/retyping.cmx tactics/setoid_replace.cmx tactics/tacinterp.cmx \
- proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
- tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \
- kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \
- toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx tactics/wcclausenv.cmx \
- tactics/equality.cmi
+ pretyping/evarutil.cmx tactics/hipattern.cmx pretyping/indrec.cmx \
+ kernel/inductive.cmx pretyping/inductiveops.cmx pretyping/instantiate.cmx \
+ proofs/logic.cmx library/nameops.cmx kernel/names.cmx \
+ pretyping/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \
+ pretyping/rawterm.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
+ tactics/setoid_replace.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \
+ pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+ kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \
+ pretyping/typing.cmx kernel/univ.cmx lib/util.cmx toplevel/vernacexpr.cmx \
+ toplevel/vernacinterp.cmx tactics/wcclausenv.cmx tactics/equality.cmi
tactics/extraargs.cmo: parsing/extend.cmi parsing/genarg.cmi \
toplevel/metasyntax.cmi parsing/pcoq.cmi lib/pp.cmi parsing/ppconstr.cmi \
parsing/pptactic.cmi parsing/printer.cmi tactics/tacinterp.cmi \
diff --git a/configure b/configure
index 232669a7d..362992fe9 100755
--- a/configure
+++ b/configure
@@ -6,9 +6,9 @@
#
##################################
-VERSION=7.3
+VERSION=7.3+1
VERSIONSI=1.0
-DATE="May 2002"
+DATE="August 2002"
# a local which command for sh
which () {
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 463f6f21d..2d30b2aa3 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -12,6 +12,7 @@ open Util
open Pp
open Term
open Names
+open Declarations
open Environ
open Esubst
@@ -385,6 +386,15 @@ let defined_rels flags env =
env ~init:(0,[])
(* else (0,[])*)
+
+let rec mind_equiv info kn1 kn2 =
+ kn1 = kn2 ||
+ match (lookup_mind kn1 info.i_env).mind_equiv with
+ Some kn1' -> mind_equiv info kn2 kn1'
+ | None -> match (lookup_mind kn2 info.i_env).mind_equiv with
+ Some kn2' -> mind_equiv info kn2' kn1
+ | None -> false
+
let create mk_cl flgs env =
{ i_flags = flgs;
i_repr = mk_cl;
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 826d58fba..d3c5e5c59 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -187,6 +187,9 @@ val whd_stack :
(* [unfold_reference] unfolds references in a [fconstr] *)
val unfold_reference : clos_infos -> table_key -> fconstr option
+(* [mind_equiv] checks whether two mutual inductives are intentionally equal *)
+val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool
+
(***********************************************************************)
(*i This is for lazy debug *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 67c0cb998..8b1170597 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -84,7 +84,9 @@ type mutual_inductive_body = {
mind_hyps : section_context;
mind_packets : one_inductive_body array;
mind_constraints : constraints;
- mind_singl : constr option }
+ mind_singl : constr option;
+ mind_equiv : kernel_name option
+ }
(* TODO: should be changed to non-coping after Term.subst_mps *)
let subst_const_body sub cb =
@@ -119,6 +121,7 @@ let subst_mind sub mib =
mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
mind_constraints = mib.mind_constraints ;
mind_singl = option_app (Term.subst_mps sub) mib.mind_singl;
+ mind_equiv = option_app (subst_kn sub) mib.mind_equiv;
}
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 9ea7e20f8..574cb04fa 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -76,7 +76,9 @@ type mutual_inductive_body = {
mind_hyps : section_context;
mind_packets : one_inductive_body array;
mind_constraints : constraints;
- mind_singl : constr option }
+ mind_singl : constr option;
+ mind_equiv : kernel_name option;
+ }
val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 036bce60b..58a117bdc 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -525,7 +525,9 @@ let build_inductive env env_ar finite inds recargs cst =
mind_hyps = hyps;
mind_packets = packets;
mind_constraints = cst;
- mind_singl = None }
+ mind_singl = None;
+ mind_equiv = None;
+ }
(***********************************************************************)
(***********************************************************************)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index cc2c37790..605f11d67 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -697,6 +697,14 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
*)
(***********************************************************************)
+(* Scrape *)
+
+let rec scrape_mind env kn =
+ match (Environ.lookup_mind kn env).mind_equiv with
+ | None -> kn
+ | Some kn' -> scrape_mind env kn'
+
+(***********************************************************************)
(* Co-fixpoints. *)
exception CoFixGuardError of guard_error
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index f279eb79a..a6ce7d42e 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -44,8 +44,8 @@ val type_of_constructor : env -> constructor -> types
val arities_of_constructors : env -> inductive -> types array
(* Transforms inductive specification into types (in nf) *)
-val arities_of_specif :
- kernel_name -> mutual_inductive_body * one_inductive_body -> types array
+val arities_of_specif : mutual_inductive ->
+ mutual_inductive_body * one_inductive_body -> types array
(* [type_case_branches env (I,args) (p:A) c] computes useful types
about the following Cases expression:
@@ -62,6 +62,10 @@ val type_case_branches :
given inductive type. *)
val check_case_info : env -> inductive -> case_info -> unit
+(* Find the ultimate inductive in the mind_equiv chain *)
+
+val scrape_mind : env -> mutual_inductive -> mutual_inductive
+
(*s Guard conditions for fix and cofix-points. *)
val check_fix : env -> fixpoint -> unit
val check_cofix : env -> cofixpoint -> unit
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 5c4b00d94..1eb74ffef 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -32,6 +32,8 @@ let rec list_fold_map2 f e = function
let e'',t1',t2' = list_fold_map2 f e' t in
e'',h1'::t1',h2'::t2'
+let type_modpath env mp =
+ strengthen env (lookup_module mp env).mod_type mp
let rec translate_modtype env mte =
match mte with
@@ -100,7 +102,7 @@ and translate_module env is_definition me =
with
| Not_path -> error_declaration_not_path mexpr
in
- MEBident mp, (lookup_module mp env).mod_type
+ MEBident mp, type_modpath env mp
in
let mtb,mod_user_type =
match me.mod_entry_type with
@@ -118,7 +120,7 @@ and translate_module env is_definition me =
and translate_mexpr env mexpr = match mexpr with
| MEident mp ->
MEBident mp,
- (lookup_module mp env).mod_type
+ type_modpath env mp
| MEfunctor (arg_id, arg_e, body_expr) ->
let arg_b = translate_modtype env arg_e in
let env' = add_module (MPbound arg_id) (module_body_of_type arg_b) env in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 1b0ff8ace..ea8a2c4e2 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -55,7 +55,7 @@ let error_not_a_module s =
let rec scrape_modtype env = function
- | MTBident ln -> scrape_modtype env (lookup_modtype ln env)
+ | MTBident kn -> scrape_modtype env (lookup_modtype kn env)
| mtb -> mtb
@@ -79,7 +79,7 @@ let destr_functor = function
let rec check_modpath_equiv env mp1 mp2 =
- if mp1=mp2 then ();
+ if mp1=mp2 then () else
let mb1 = lookup_module mp1 env in
match mb1.mod_equiv with
| None ->
@@ -149,3 +149,52 @@ and add_module mp mb env =
| MTBfunsig _ -> env
+let strengthen_const env mp l cb = match cb.const_body with
+ | Some _ -> cb
+ | None -> {cb with const_body = Some (mkConst (make_kn mp empty_dirpath l))}
+
+let strengthen_mind env mp l mib = match mib.mind_equiv with
+ | Some _ -> mib
+ | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
+
+let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with
+ | MTBident _ -> anomaly "scrape_modtype does not work!"
+ | MTBfunsig _ -> mtb
+ | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp)
+and strengthen_mod env mp (mtb,mpo) =
+ let mtb' = strengthen_mtb env mp mtb in
+ let mpo' = match mpo with
+ | Some _ -> mpo
+ | None -> Some mp
+ in
+ (mtb',mpo')
+and strengthen_sig env msid sign mp = match sign with
+ | [] -> []
+ | (l,SPBconst cb) :: rest ->
+ let item' = l,SPBconst (strengthen_const env mp l cb) in
+ let rest' = strengthen_sig env msid rest mp in
+ item'::rest'
+ | (l,SPBmind mib) :: rest ->
+ let item' = l,SPBmind (strengthen_mind env mp l mib) in
+ let rest' = strengthen_sig env msid rest mp in
+ item'::rest'
+ | (l,SPBmodule mb) :: rest ->
+ let mp' = MPdot (mp,l) in
+ let item' = l,SPBmodule (strengthen_mod env mp' mb) in
+ let env' = add_module
+ (MPdot (MPself msid,l))
+ (module_body_of_spec mb)
+ env
+ in
+ let rest' = strengthen_sig env' msid rest mp in
+ item'::rest'
+ | (l,SPBmodtype mty as item) :: rest ->
+ let env' = add_modtype
+ (make_kn (MPself msid) empty_dirpath l)
+ mty
+ env
+ in
+ let rest' = strengthen_sig env' msid rest mp in
+ item::rest'
+
+let strengthen env mtb mp = strengthen_mtb env mp mtb
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 240144785..7cd22c57c 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -51,6 +51,8 @@ val add_module :
val check_modpath_equiv : env -> module_path -> module_path -> unit
+val strengthen : env -> module_type_body -> module_path -> module_type_body
+
val error_existing_label : label -> 'a
val error_declaration_not_path : module_expr -> 'a
@@ -62,6 +64,8 @@ val error_not_a_functor : module_expr -> 'a
val error_incompatible_modtypes :
module_type_body -> module_type_body -> 'a
+val error_not_equal : module_path -> module_path -> 'a
+
val error_not_match : label -> specification_body -> 'a
val error_incompatible_labels : label -> label -> 'a
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4512546ae..a452138fc 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -244,14 +244,15 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in
convert_stacks infos lft1 lft2 v1 v2 u3
*)
- | (FInd op1, FInd op2) ->
- if op1 = op2 then
+ | (FInd (kn1,i1), FInd (kn2,i2)) ->
+ if i1 = i2 && mind_equiv infos kn1 kn2
+ then
convert_stacks infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
- | (FConstruct op1, FConstruct op2) ->
- if op1 = op2
- then
+ | (FConstruct ((kn1,i1),j1), FConstruct ((kn2,i2),j2)) ->
+ if i1 = i2 && j1 = j2 && mind_equiv infos kn1 kn2
+ then
convert_stacks infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 4b4ae17cf..f62725c70 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -103,8 +103,6 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
let cst = check_conv cst conv env p1.mind_nf_arity p2.mind_nf_arity in
cst
in
- (* this function uses mis_something and the others do not.
- Perhaps we should uniformize it at some point... *)
let check_cons_types i cst p1 p2 =
array_fold_left2
(fun cst t1 t2 -> check_conv cst conv env t1 t2)
@@ -113,28 +111,41 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
(arities_of_specif kn (mib2,p2))
in
let check f = if f mib1 <> f mib2 then error () in
- check (fun mib -> mib.mind_finite);
- check (fun mib -> mib.mind_ntypes);
- assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
- assert (Array.length mib1.mind_packets >= 1
+ check (fun mib -> mib.mind_finite);
+ check (fun mib -> mib.mind_ntypes);
+ assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
+ assert (Array.length mib1.mind_packets >= 1
&& Array.length mib2.mind_packets >= 1);
- check (fun mib -> mib.mind_packets.(0).mind_nparams);
- check (fun mib -> mib.mind_packets.(0).mind_params_ctxt);
- (* TODO: we should allow renaming of parameters at least ! *)
- let cst = match mib1.mind_singl, mib2.mind_singl with
- None, None -> cst
- | Some c1, Some c2 -> check_conv cst conv env c1 c2
- | _ -> error ()
- in
- (* we first check simple things *)
- let cst =
- array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets
- in
- (* and constructor types in the end *)
- let cst =
- array_fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets
- in
- cst
+
+ (* TODO: we should allow renaming of parameters at least ! *)
+ check (fun mib -> mib.mind_packets.(0).mind_nparams);
+ check (fun mib -> mib.mind_packets.(0).mind_params_ctxt);
+
+ begin
+ match mib2.mind_equiv with
+ | None -> ()
+ | Some kn2' ->
+ let kn2 = scrape_mind env kn2' in
+ let kn1 = match mib1.mind_equiv with
+ None -> kn
+ | Some kn1' -> scrape_mind env kn1'
+ in
+ if kn1 <> kn2 then error ()
+ end;
+ let cst = match mib1.mind_singl, mib2.mind_singl with
+ | None, None -> cst
+ | Some c1, Some c2 -> check_conv cst conv env c1 c2
+ | _ -> error ()
+ in
+ (* we first check simple things *)
+ let cst =
+ array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets
+ in
+ (* and constructor types in the end *)
+ let cst =
+ array_fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets
+ in
+ cst
let check_constant cst env msid1 l info1 cb2 spec2 =
let error () = error_not_match l spec2 in
@@ -172,12 +183,14 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
*)
let rec check_modules cst env msid1 l msb1 msb2 =
- let cst = check_modtypes cst env (fst msb1) (fst msb2) false in
+ let mp = (MPdot(MPself msid1,l)) in
+ let mty1 = strengthen env (fst msb1) mp in
+ let cst = check_modtypes cst env mty1 (fst msb2) false in
begin
match (snd msb1), (snd msb2) with
| _, None -> ()
| None, Some mp2 ->
- check_modpath_equiv env (MPdot(MPself msid1,l)) mp2
+ check_modpath_equiv env mp mp2
| Some mp1, Some mp2 ->
check_modpath_equiv env mp1 mp2
end;
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 7b5adfdc9..89a826c92 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -403,7 +403,8 @@ let start_module id argids args res_o =
let fs = Summary.freeze_summaries () in
process_module_bindings argids args;
openmod_info:=(mbids,res_o);
- Lib.start_module id mp fs;
+ let prefix = Lib.start_module id mp fs in
+ Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
Lib.add_frozen_state ()
@@ -515,7 +516,8 @@ let start_modtype id argids args =
let fs= Summary.freeze_summaries () in
process_module_bindings argids args;
openmodtype_info := (List.map fst args);
- Lib.start_modtype id mp fs;
+ let prefix = Lib.start_modtype id mp fs in
+ Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
Lib.add_frozen_state ()
diff --git a/library/lib.ml b/library/lib.ml
index 286133305..323ca60de 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -268,7 +268,8 @@ let start_module id mp nametab =
if Nametab.exists_module dir then
errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
add_entry oname (OpenedModule (prefix,nametab));
- path_prefix := prefix
+ path_prefix := prefix;
+ prefix
(* add_frozen_state () must be called in declaremods *)
let end_module id =
@@ -303,7 +304,8 @@ let start_modtype id mp nametab =
if Nametab.exists_cci sp then
errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ;
add_entry name (OpenedModtype (prefix,nametab));
- path_prefix := prefix
+ path_prefix := prefix;
+ prefix
let end_modtype id =
let sp,nametab =
diff --git a/library/lib.mli b/library/lib.mli
index 90f111c4b..075be2890 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -123,11 +123,13 @@ val module_dp : unit -> dir_path
(*s Modules and module types *)
-val start_module : module_ident -> module_path -> Summary.frozen -> unit
+val start_module :
+ module_ident -> module_path -> Summary.frozen -> object_prefix
val end_module : module_ident
-> object_name * object_prefix * Summary.frozen * library_segment
-val start_modtype : module_ident -> module_path -> Summary.frozen -> unit
+val start_modtype :
+ module_ident -> module_path -> Summary.frozen -> object_prefix
val end_modtype : module_ident
-> object_name * object_prefix * Summary.frozen * library_segment
diff --git a/library/nametab.ml b/library/nametab.ml
index bc419a237..1f8111a2c 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -106,7 +106,7 @@ let push_many vis tab dir o =
| Absolute _ ->
(* This is an absolute name, we must keep it otherwise it may
become unaccessible forever *)
- warning "Trying to zaslonic an absolute name!"; current
+ warning "Trying to mask an absolute name!"; current
| Nothing
| Relative _ -> Relative o
else current
@@ -118,7 +118,7 @@ let push_many vis tab dir o =
(* This is an absolute name, we must keep it otherwise it may
become unaccessible forever *)
(* But ours is also absolute! This is an error! *)
- error "Trying to zaslonic an absolute name!"
+ error "Trying to mask an absolute name!"
| Nothing
| Relative _ -> Absolute o, dirmap
in
@@ -137,7 +137,7 @@ let push_one vis tab dir o =
| Absolute _ ->
(* This is an absolute name, we must keep it otherwise it may
become unaccessible forever *)
- error "Trying to zaslonic an absolute name!"
+ error "Trying to mask an absolute name!"
| Nothing
| Relative _ -> Relative o
in
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 6554659f3..159b082f0 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -293,10 +293,16 @@ let print_constant with_values sep sp =
let print_inductive sp = (print_mutual sp ++ fnl ())
let print_syntactic_def sep kn =
- let _,_,l = repr_kn kn in
+ let l = label kn in
let c = Syntax_def.search_syntactic_definition kn in
(str" Syntactic Definition " ++ pr_lab l ++ str sep ++ pr_rawterm c ++ fnl ())
+let print_module with_values kn =
+ str "Module " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl ()
+
+let print_modtype kn =
+ str "Module Type " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl ()
+
let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
let tag = object_tag lobj in
match (oname,tag) with
@@ -306,6 +312,10 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
print_constant with_values sep kn
| (_,"INDUCTIVE") ->
print_inductive kn
+ | (_,"MODULE") ->
+ print_module with_values kn
+ | (_,"MODULE TYPE") ->
+ print_modtype kn
| (_,"AUTOHINT") ->
(* (str" Hint Marker" ++ fnl ())*)
(mt ())
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f3e2ac0f1..8b41ba038 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -383,8 +383,11 @@ let vernac_declare_module id bl mty_ast_o mexpr_ast_o =
Astmod.interp_module_decl evd env bl mty_ast_o mexpr_ast_o
in
let argids, args = List.split arglist
- in (* We check the state of the system (in module, in module type)
- and what parts are supplied *)
+ in (* We check the state of the system (in section, in module type)
+ and what module information is supplied *)
+ if Lib.sections_are_opened () then
+ error "Modules and Module Types are not allowed inside sections";
+
match Lib.is_specification (), base_mty_o, base_mexpr_o with
| _, None, None
| false, _, None ->
@@ -393,6 +396,7 @@ let vernac_declare_module id bl mty_ast_o mexpr_ast_o =
("Interactive Module "^ string_of_id id ^" started")
| true, Some _, None
+ | true, _, Some (MEident _)
| false, _, Some _ ->
let mexpr_o =
option_app
@@ -416,7 +420,7 @@ let vernac_declare_module id bl mty_ast_o mexpr_ast_o =
if_verbose message
("Module "^ string_of_id id ^" is defined")
- | true, _, Some _ ->
+ | true, _, Some (MEfunctor _ | MEapply _ | MEstruct _) ->
error "Module definition not allowed in a Module Type"
@@ -434,15 +438,17 @@ let vernac_declare_module_type id bl mty_ast_o =
Astmod.interp_module_decl evd env bl mty_ast_o None
in
let argids, args = List.split arglist
- in (* We check the state of the system (in module, in module type)
- and what parts are supplied *)
- match Lib.is_specification (), base_mty_o with
- | _, None ->
+ in
+ if Lib.sections_are_opened () then
+ error "Modules and Module Types are not allowed inside sections";
+
+ match base_mty_o with
+ | None ->
Declaremods.start_modtype id argids args;
if_verbose message
("Interactive Module Type "^ string_of_id id ^" started")
- | _, Some base_mty ->
+ | Some base_mty ->
let mty =
List.fold_right
(fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 20:29:28 +0000