diff options
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 22 |
1 files changed, 10 insertions, 12 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index d5f0b7bff6..7bc5d090b4 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -140,7 +140,7 @@ let rec constr_expr_eq e1 e2 = in List.equal field_eq l1 l2 | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> - (** Don't care about the case_style *) + (* Don't care about the case_style *) Option.equal constr_expr_eq r1 r2 && List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 @@ -220,7 +220,7 @@ and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> - (** Don't care about the [binder_kind] *) + (* Don't care about the [binder_kind] *) List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false @@ -258,7 +258,6 @@ let local_binders_loc bll = match bll with | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll)) (** Folds and maps *) - let is_constructor id = try Globnames.isConstructRef (Smartlocate.global_of_extended_global @@ -367,6 +366,14 @@ let free_vars_of_constr_expr c = | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c in aux [] Id.Set.empty c +let names_of_constr_expr c = + let vars = ref Id.Set.empty in + let rec aux () () = function + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + let id = qualid_basename qid in vars := Id.Set.add id !vars + | c -> fold_constr_expr_with_binders (fun a () -> vars := Id.Set.add a !vars) aux () () c + in aux () () c; !vars + let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c) (* Used in correctness and interface *) @@ -604,15 +611,6 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr" (str "This expression should be coercible to a pattern.")) c -let asymmetric_patterns = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "no parameters in constructors"; - Goptions.optkey = ["Asymmetric";"Patterns"]; - Goptions.optread = (fun () -> !asymmetric_patterns); - Goptions.optwrite = (fun a -> asymmetric_patterns:=a); -} - (** Local universe and constraint declarations. *) let interp_univ_constraints env evd cstrs = |