diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 09:59:16 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 09:59:16 +0100 |
| commit | 4fb4f1adf18648b4fb561986379e033b00423148 (patch) | |
| tree | 876f561f9310b9e15f3ac20ca71f9dd28f90b157 /intf | |
| parent | 349944eb8e3abd51dc2b94051a887253a2ae9198 (diff) | |
| parent | de988641848ecb26f749fbc3f50ce9194db46a4c (diff) | |
Merge PR #6651: Use r.(p) syntax to print primitive projections.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 1 | ||||
| -rw-r--r-- | intf/glob_term.ml | 1 | ||||
| -rw-r--r-- | intf/notation_term.ml | 1 | ||||
| -rw-r--r-- | intf/pattern.ml | 2 |
4 files changed, 4 insertions, 1 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 8bcdbcc0e..fbf9e248a 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -97,6 +97,7 @@ and constr_expr_r = | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr + | CProj of reference * constr_expr and constr_expr = constr_expr_r CAst.t and case_expr = constr_expr (* expression that is being matched *) diff --git a/intf/glob_term.ml b/intf/glob_term.ml index f311d33b8..61bbe2c26 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -55,6 +55,7 @@ type 'a glob_constr_r = | GSort of glob_sort | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type + | GProj of Projection.t * 'a glob_constr_g and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 7823d3feb..cad6f4b82 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -43,6 +43,7 @@ type notation_constr = notation_constr array * notation_constr array | NSort of glob_sort | NCast of notation_constr * notation_constr cast_type + | NProj of Projection.t * notation_constr (** Note concerning NList: first constr is iterator, second is terminator; first id is where each argument of the list has to be substituted diff --git a/intf/pattern.ml b/intf/pattern.ml index 20636accf..64873a039 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -26,7 +26,7 @@ type constr_pattern = | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of patvar * constr_pattern list - | PProj of projection * constr_pattern + | PProj of Projection.t * constr_pattern | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern |