diff options
| author | Matthieu Sozeau | 2014-07-01 22:50:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-01 22:52:08 +0200 |
| commit | 4c97e4ce19ca4c387039cfdcb4f24658100230b0 (patch) | |
| tree | 8e6367b1936d842b3e56283abc25de2342452884 /toplevel | |
| parent | 3d2582eeb492fb21b7136016bf4c1a0463dc15c2 (diff) | |
Add toplevel commands to declare global universes and constraints.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 3 | ||||
| -rw-r--r-- | toplevel/command.mli | 3 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 5 |
3 files changed, 11 insertions, 0 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index faa4b12dfd..95ddf1fb06 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -38,6 +38,9 @@ open Indschemes open Misctypes open Vernacexpr +let do_universe l = Declare.do_universe l +let do_constraint l = Declare.do_constraint l + let rec under_binders env f n c = if Int.equal n 0 then f env Evd.empty c else match kind_of_term c with diff --git a/toplevel/command.mli b/toplevel/command.mli index 4d1c749079..d14af73946 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -21,6 +21,9 @@ open Pfedit (** This file is about the interpretation of raw commands into typed ones and top-level declaration of the main Gallina objects *) +val do_universe : Id.t Loc.located list -> unit +val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit + (** {6 Hooks for Pcoq} *) val set_declare_definition_hook : (definition_entry -> unit) -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b1ed564d81..1d05f4e622 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -605,6 +605,9 @@ let vernac_combined_scheme lid l = List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l); Indschemes.do_combined_scheme lid l +let vernac_universe l = do_universe l +let vernac_constraint l = do_constraint l + (**********************) (* Modules *) @@ -1721,6 +1724,8 @@ let interp ?proof locality poly c = | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l + | VernacUniverse l -> vernac_universe l + | VernacConstraint l -> vernac_constraint l (* Modules *) | VernacDeclareModule (export,lid,bl,mtyo) -> |