diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-25 22:43:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-09 23:28:09 +0100 |
| commit | b1d749e59444f86e40f897c41739168bb1b1b9b3 (patch) | |
| tree | ade1ab73a9c2066302145bb3781a39b5d46b4513 /interp/declare.ml | |
| parent | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (diff) | |
[located] Push inner locations in `reference` to a CAst.t node.
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 7dd73fbb5..c55a6c69b 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -592,15 +592,10 @@ let input_constraints : constraint_decl -> Libobject.obj = discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } -let loc_of_glob_level = function - | Misctypes.GType (Misctypes.UNamed n) -> Libnames.loc_of_reference n - | _ -> None - let do_constraint poly l = let u_of_id x = let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - let loc = loc_of_glob_level x in - loc, Universes.is_polymorphic level, level + Universes.is_polymorphic level, level in let in_section = Lib.sections_are_opened () in let () = @@ -608,18 +603,17 @@ let do_constraint poly l = user_err ~hdr:"Constraint" (str"Cannot declare polymorphic constraints outside sections") in - let check_poly ?loc p loc' p' = + let check_poly p p' = if poly then () else if p || p' then - let loc = if p then loc else loc' in - user_err ?loc ~hdr:"Constraint" + user_err ~hdr:"Constraint" (str "Cannot declare a global constraint on " ++ str "a polymorphic universe, use " ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let ploc, p, lu = u_of_id l and rloc, p', ru = u_of_id r in - check_poly ?loc:ploc p rloc p'; + let p, lu = u_of_id l and p', ru = u_of_id r in + check_poly p p'; Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in |