diff options
| author | Hugo Herbelin | 2017-02-02 17:10:43 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-24 12:17:35 +0100 |
| commit | 8965549b994262a27f5dd204d9c4012501d1a040 (patch) | |
| tree | 5bc257b9aa36f9b4be0e9c8788cdbd526508db60 | |
| parent | a1e5a87c9d4368fe17d93988b010acfb1c96771b (diff) | |
Standardized the order of constructors for binders: Assum then Def.
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | 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 = |