diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checker.ml | 4 | ||||
| -rw-r--r-- | checker/declarations.ml | 36 | ||||
| -rw-r--r-- | checker/dune | 2 | ||||
| -rw-r--r-- | checker/indtypes.ml | 2 | ||||
| -rw-r--r-- | checker/modops.ml | 2 | ||||
| -rw-r--r-- | checker/univ.ml | 5 | ||||
| -rw-r--r-- | checker/values.ml | 2 |
7 files changed, 28 insertions, 25 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index d3d114d7d7..8a5220c9ca 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -243,7 +243,9 @@ let explain_exn = function | Invalid_argument s -> hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ()) | Sys.Break -> - hov 0 (fnl () ++ str "User interrupt.") + hov 0 (fnl () ++ str "User interrupt.") + | Univ.AlreadyDeclared -> + hov 0 (str "Error: Multiply declared universe.") | Univ.UniverseInconsistency (o,u,v) -> let msg = if !Flags.debug (*!Constrextern.print_universes*) then diff --git a/checker/declarations.ml b/checker/declarations.ml index 03fee1ab51..93d5f8bfa2 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -70,12 +70,12 @@ let solve_delta_kn resolve kn = | Equiv kn1 -> kn1 | Inline _ -> raise Not_found with Not_found -> - let mp,dir,l = KerName.repr kn in + let mp,l = KerName.repr kn in let new_mp = find_prefix resolve mp in if mp == new_mp then kn else - KerName.make new_mp dir l + KerName.make new_mp l let gen_of_delta resolve x kn fix_can = let new_kn = solve_delta_kn resolve kn in @@ -129,17 +129,17 @@ let subst_mp sub mp = | Some (mp',_) -> mp' let subst_kn_delta sub kn = - let mp,dir,l = KerName.repr kn in + let mp,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',resolve) -> - solve_delta_kn resolve (KerName.make mp' dir l) + solve_delta_kn resolve (KerName.make mp' l) | None -> kn let subst_kn sub kn = - let mp,dir,l = KerName.repr kn in + let mp,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',_) -> - KerName.make mp' dir l + KerName.make mp' l | None -> kn exception No_subst @@ -156,16 +156,16 @@ let gen_subst_mp f sub mp1 mp2 = | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2 -let make_mind_equiv mpu mpc dir l = - let knu = KerName.make mpu dir l in +let make_mind_equiv mpu mpc l = + let knu = KerName.make mpu l in if mpu == mpc then MutInd.make1 knu - else MutInd.make knu (KerName.make mpc dir l) + else MutInd.make knu (KerName.make mpc l) let subst_ind sub mind = let kn1,kn2 = MutInd.user mind, MutInd.canonical mind in - let mp1,dir,l = KerName.repr kn1 in - let mp2,_,_ = KerName.repr kn2 in - let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in + let mp1,l = KerName.repr kn1 in + let mp2,_ = KerName.repr kn2 in + let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 l in try let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in match side with @@ -173,16 +173,16 @@ let subst_ind sub mind = | Canonical -> mind_of_delta2 resolve mind' with No_subst -> mind -let make_con_equiv mpu mpc dir l = - let knu = KerName.make mpu dir l in +let make_con_equiv mpu mpc l = + let knu = KerName.make mpu l in if mpu == mpc then Constant.make1 knu - else Constant.make knu (KerName.make mpc dir l) + else Constant.make knu (KerName.make mpc l) let subst_con0 sub con u = let kn1,kn2 = Constant.user con, Constant.canonical con in - let mp1,dir,l = KerName.repr kn1 in - let mp2,_,_ = KerName.repr kn2 in - let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in + let mp1,l = KerName.repr kn1 in + let mp2,_ = KerName.repr kn2 in + let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 l in let dup con = con, Const (con, u) in let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in match constant_of_delta_with_inline resolve con' with diff --git a/checker/dune b/checker/dune index d520171f98..ebb3dd7583 100644 --- a/checker/dune +++ b/checker/dune @@ -19,6 +19,7 @@ (executable (name main) (public_name coqchk) + (package coq) (modules main) (flags :standard -open Checklib) (libraries coq.checklib)) @@ -26,6 +27,7 @@ (executable (name votour) (public_name votour) + (package coq) (modules votour) (flags :standard -open Checklib) (libraries coq.checklib)) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 1fd86bc368..0478765a81 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -34,7 +34,7 @@ let string_of_mp mp = if !Flags.debug then debug_string_of_mp mp else string_of_mp mp let prkn kn = - let (mp,_,l) = KerName.repr kn in + let (mp,l) = KerName.repr kn in str(string_of_mp mp ^ "." ^ Label.to_string l) let prcon c = let ck = Constant.canonical c in diff --git a/checker/modops.ml b/checker/modops.ml index b92d7bbf1f..541d009ff9 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -55,7 +55,7 @@ let module_body_of_type mp mtb = let rec add_structure mp sign resolver env = let add_one env (l,elem) = - let kn = KerName.make2 mp l in + let kn = KerName.make mp l in let con = Constant.make1 kn in let mind = mind_of_delta resolver (MutInd.make1 kn) in match elem with diff --git a/checker/univ.ml b/checker/univ.ml index e50e883adf..a0511ad21b 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1088,14 +1088,13 @@ let subst_univs_universe fn ul = let merge_context strict ctx g = let g = Array.fold_left - (* Be lenient, module typing reintroduces universes and - constraints due to includes *) - (fun g v -> try add_universe v strict g with AlreadyDeclared -> g) + (fun g v -> add_universe v strict g) g (UContext.instance ctx) in merge_constraints (UContext.constraints ctx) g let merge_context_set strict ctx g = let g = LSet.fold + (* Include and side effects still have double-declared universes *) (fun v g -> try add_universe v strict g with AlreadyDeclared -> g) (ContextSet.levels ctx) g in merge_constraints (ContextSet.constraints ctx) g diff --git a/checker/values.ml b/checker/values.ml index 35027d5bfb..24f10b7a87 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -98,7 +98,7 @@ let rec v_mp = Sum("module_path",0, [|[|v_dp|]; [|v_uid|]; [|v_mp;v_id|]|]) -let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|] +let v_kn = v_tuple "kernel_name" [|v_mp;v_id;Int|] let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|] let v_ind = v_tuple "inductive" [|v_cst;Int|] let v_cons = v_tuple "constructor" [|v_ind;Int|] |