diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-02 18:24:58 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 12:17:35 +0100 |
| commit | 648ce5e08f7245f2a775abd1304783c4167e9f2e (patch) | |
| tree | 7d57ea1c188f3e2892e27e544dbadf48de2c975b /intf/constrexpr.mli | |
| parent | 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b (diff) | |
Unifying standard "constr_level" names for constructors of local_binder_expr.
RawLocal -> CLocal
Diffstat (limited to 'intf/constrexpr.mli')
| -rw-r--r-- | intf/constrexpr.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index c2ace9dc2..d1b5697d7 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -123,9 +123,9 @@ and recursion_order_expr = (** Anonymous defs allowed ?? *) and local_binder_expr = - | LocalRawAssum of Name.t located list * binder_kind * constr_expr - | LocalRawDef of Name.t located * constr_expr - | LocalRawPattern of Loc.t * cases_pattern_expr * constr_expr option + | CLocalAssum of Name.t located list * binder_kind * constr_expr + | CLocalDef of Name.t located * constr_expr + | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option and constr_notation_substitution = constr_expr list * (** for constr subterms *) |