aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
authorHugo Herbelin2017-02-02 17:10:43 +0100
committerMaxime Dénès2017-03-24 12:17:35 +0100
commit8965549b994262a27f5dd204d9c4012501d1a040 (patch)
tree5bc257b9aa36f9b4be0e9c8788cdbd526508db60 /intf
parenta1e5a87c9d4368fe17d93988b010acfb1c96771b (diff)
Standardized the order of constructors for binders: Assum then Def.
Diffstat (limited to 'intf')
-rw-r--r--intf/constrexpr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 1499ed70e9..f7aa722799 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -123,8 +123,8 @@ and recursion_order_expr =
(** Anonymous defs allowed ?? *)
and local_binder =
- | LocalRawDef of Name.t located * constr_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
and constr_notation_substitution =