diff options
| author | Maxime Dénès | 2016-09-30 12:51:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-30 12:51:16 +0200 |
| commit | 7543449792d417a92092b692986d62b622b78ffc (patch) | |
| tree | 8244b6c3efa88abe12ab990a4ae4b3d0af8f5dc1 /library | |
| parent | bff880ffb6ef33c99a96e7925c995b31b1497e6a (diff) | |
| parent | 9615c025a2a09b69f2001d44a66a1fddef74e680 (diff) | |
Merge remote-tracking branch 'github/pr/299' into v8.6
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 24 | ||||
| -rw-r--r-- | library/declare.mli | 4 |
2 files changed, 19 insertions, 9 deletions
diff --git a/library/declare.ml b/library/declare.ml index 7d32b93dc5..c5b83c11a0 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -507,12 +507,20 @@ let input_constraints : constraint_decl -> Libobject.obj = classify_function = (fun a -> Keep a) } let do_constraint poly l = - let u_of_id = - let names, _ = Universes.global_universe_names () in - fun (loc, id) -> - try Idmap.find id names - with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + let open Misctypes in + let u_of_id x = + match x with + | GProp -> Loc.dummy_loc, (false, Univ.Level.prop) + | GSet -> Loc.dummy_loc, (false, Univ.Level.set) + | GType None -> + user_err_loc (Loc.dummy_loc, "Constraint", + str "Cannot declare constraints on anonymous universes") + | GType (Some (loc, id)) -> + let id = Id.of_string id in + let names, _ = Universes.global_universe_names () in + try loc, Idmap.find id names + with Not_found -> + user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) in let in_section = Lib.sections_are_opened () in let () = @@ -530,8 +538,8 @@ let do_constraint poly l = ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let p, lu = u_of_id l and p', ru = u_of_id r in - check_poly (fst l) p (fst r) p'; + let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in + check_poly ploc p rloc p'; Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in diff --git a/library/declare.mli b/library/declare.mli index e614f5206a..f70d594d7e 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -92,4 +92,6 @@ val exists_name : Id.t -> bool val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit val do_universe : polymorphic -> Id.t Loc.located list -> unit -val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_constraint : polymorphic -> + (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> + unit |