diff options
| author | Pierre-Marie Pédrot | 2016-02-19 16:34:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-19 16:34:13 +0100 |
| commit | a4b457bef4290fed3f2869795f1539de53b3805a (patch) | |
| tree | 4cc684e352b4857156b32bc913ea05847b8cbb4e /engine/sigma.mli | |
| parent | 82e4e8f2afbff4f1dbecb8a37e3c1c18a41c754f (diff) | |
| parent | bd0dc480ec02352b83e335ed2209abcf3d0f89eb (diff) | |
Merge branch 'located-universes'
Diffstat (limited to 'engine/sigma.mli')
| -rw-r--r-- | engine/sigma.mli | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/engine/sigma.mli b/engine/sigma.mli index d7ae2e4ac9..643bea4036 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -66,23 +66,23 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) -val new_univ_level_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> - 'r t -> (Univ.universe_level, 'r) sigma -val new_univ_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> - 'r t -> (Univ.universe, 'r) sigma -val new_sort_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> - 'r t -> (Sorts.t, 'r) sigma - -val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env -> +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> + Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma +val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> + Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma +val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> + Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma + +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env -> 'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma val fresh_constant_instance : - Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma + ?loc:Loc.t -> Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma val fresh_inductive_instance : - Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma -val fresh_constructor_instance : Environ.env -> 'r t -> constructor -> + ?loc:Loc.t -> Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma +val fresh_constructor_instance : ?loc:Loc.t -> Environ.env -> 'r t -> constructor -> (pconstructor, 'r) sigma -val fresh_global : ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> +val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> 'r t -> Globnames.global_reference -> (constr, 'r) sigma (** FILLME *) |