From 8965549b994262a27f5dd204d9c4012501d1a040 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 17:10:43 +0100
Subject: Standardized the order of constructors for binders: Assum then Def.

---
 interp/constrintern.ml | 2 +-
 intf/constrexpr.mli    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c037da3059..ff0cdd49f5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -456,8 +456,8 @@ let intern_local_pattern intern lvar env p =
     env (free_vars_of_pat [] p)
 
 type extended_glob_local_binder =
-  | GLocalDef of (Loc.t * (Name.t * binding_kind * glob_constr * glob_constr))
   | GLocalAssum of (Loc.t * (Name.t * binding_kind * glob_constr))
+  | GLocalDef of (Loc.t * (Name.t * binding_kind * glob_constr * glob_constr))
   | GLocalPattern of
       (Loc.t * (cases_pattern * Id.t list) *
          (bool ref *
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 =
-- 
cgit v1.2.3