diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 16:57:38 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 16:57:38 +0200 |
commit | 3c47248abc27aa9c64120db30dcb0d7bf945bc70 (patch) | |
tree | 0dd3a804e1924862390a7f78abc9a8a119127f9c /interp | |
parent | ceb68d1d643ac65f500e0201f61e73cf22e6e2fb (diff) | |
parent | 1bc1cba7a759a285131a3ed6ea8979716700b856 (diff) |
Merge remote-tracking branch 'github/pr/283' into trunk
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrexpr_ops.ml | 8 | ||||
-rw-r--r-- | interp/constrexpr_ops.mli | 4 | ||||
-rw-r--r-- | interp/constrextern.ml | 4 | ||||
-rw-r--r-- | interp/constrintern.ml | 2 | ||||
-rw-r--r-- | interp/constrintern.mli | 2 | ||||
-rw-r--r-- | interp/notation_ops.ml | 14 | ||||
-rw-r--r-- | interp/notation_ops.mli | 2 |
7 files changed, 18 insertions, 18 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 59c24900d..2644a56b3 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -17,7 +17,7 @@ open Decl_kinds (***********************) (* For binders parsing *) -let binding_kind_eq bk1 bk2 = match bk1, bk2 with +let implicit_status_eq bk1 bk2 = match bk1, bk2 with | Explicit, Explicit -> true | Implicit, Implicit -> true | _ -> false @@ -28,9 +28,9 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with | _ -> false let binder_kind_eq b1 b2 = match b1, b2 with -| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2 +| Default bk1, Default bk2 -> implicit_status_eq bk1 bk2 | Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) -> - binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 && + implicit_status_eq bk1 bk2 && implicit_status_eq ck1 ck2 && (if b1 then b2 else not b2) | _ -> false @@ -165,7 +165,7 @@ let rec constr_expr_eq e1 e2 = | CPrim(_,i1), CPrim(_,i2) -> prim_token_eq i1 i2 | CGeneralization (_, bk1, ak1, e1), CGeneralization (_, bk2, ak2, e2) -> - binding_kind_eq bk1 bk2 && + implicit_status_eq bk1 bk2 && Option.equal abstraction_kind_eq ak1 ak2 && constr_expr_eq e1 e2 | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) -> diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index a92da035f..bfe546ba5 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -26,8 +26,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool val local_binder_eq : local_binder -> local_binder -> bool (** Equality on [local_binder]. Same properties as [constr_expr_eq]. *) -val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool -(** Equality on [binding_kind] *) +val implicit_status_eq : Decl_kinds.implicit_status -> Decl_kinds.implicit_status -> bool +(** Equality on [implicit_status] *) val binder_kind_eq : binder_kind -> binder_kind -> bool (** Equality on [binder_kind] *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f7fcbb4ee..62cb62f49 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -808,7 +808,7 @@ and factorize_prod scopes vars na bk aty c = let c = extern_typ scopes vars c in match na, c with | Name id, CProdN (loc,[nal,Default bk',ty],c) - when binding_kind_eq bk bk' && constr_expr_eq aty ty + when implicit_status_eq bk bk' && constr_expr_eq aty ty && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> nal,c | _ -> @@ -818,7 +818,7 @@ and factorize_lambda inctx scopes vars na bk aty c = let c = sub_extern inctx scopes vars c in match c with | CLambdaN (loc,[nal,Default bk',ty],c) - when binding_kind_eq bk bk' && constr_expr_eq aty ty + when implicit_status_eq bk bk' && constr_expr_eq aty ty && not (occur_name na ty) (* avoid na in ty escapes scope *) -> nal,c | _ -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0e5602078..863f33b18 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -65,7 +65,7 @@ type var_internalization_data = type internalization_env = (var_internalization_data) Id.Map.t -type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) +type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr) type ltac_sign = { ltac_vars : Id.Set.t; diff --git a/interp/constrintern.mli b/interp/constrintern.mli index eea76aa31..718aa753e 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -75,7 +75,7 @@ type ltac_sign = { val empty_ltac_sign : ltac_sign -type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) +type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr) (** {6 Internalization performs interpretation of global names and notations } *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 6b29b6d3d..c65d43db3 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -29,10 +29,10 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1) | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> + when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 -> on_true_do (f ty1 ty2 && f c1 c2) add na1 | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> + when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 -> on_true_do (f ty1 ty2 && f c1 c2) add na1 | GHole _, GHole _ -> true | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2 @@ -772,18 +772,18 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) | GHole _, _ -> v' | _, GHole _ -> v | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in - let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in + let unify_implicit_status bk bk' = if bk == bk' then bk' else raise No_match in let unify_binder alp b b' = match b, b' with | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) -> let alp, na = unify_name alp na na' in - alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t') + alp, (Inl na, unify_implicit_status bk bk', None, unify_term alp t t') | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) -> let alp, na = unify_name alp na na' in - alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t') + alp, (Inl na, unify_implicit_status bk bk', Some (unify_term alp c c'), unify_term alp t t') | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) -> let alp, p = unify_pat alp p p' in - alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t') + alp, (Inr p, unify_implicit_status bk bk', None, unify_term alp t t') | _ -> raise No_match in let rec unify alp bl bl' = match bl, bl' with @@ -1122,7 +1122,7 @@ let term_of_binder = function | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) type glob_decl2 = - (name, cases_pattern) Util.union * Decl_kinds.binding_kind * + (name, cases_pattern) Util.union * Decl_kinds.implicit_status * glob_constr option * glob_constr let match_notation_constr u c (metas,pat) = diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 854e222e3..6428ccab6 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -48,7 +48,7 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr exception No_match type glob_decl2 = - (name, cases_pattern) Util.union * Decl_kinds.binding_kind * + (name, cases_pattern) Util.union * Decl_kinds.implicit_status * glob_constr option * glob_constr val match_notation_constr : bool -> glob_constr -> interpretation -> (glob_constr * subscopes) list * (glob_constr list * subscopes) list * |