diff options
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 8b78a91b5b..da04d8786b 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -173,10 +173,12 @@ let rec constr_expr_eq e1 e2 = | CDelimiters(s1,e1), CDelimiters(s2,e2) -> String.equal s1 s2 && constr_expr_eq e1 e2 + | CProj(p1,c1), CProj(p2,c2) -> + eq_reference p1 p2 && constr_expr_eq c1 c2 | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _ | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _ | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _ - | CGeneralization _ | CDelimiters _), _ -> false + | CGeneralization _ | CDelimiters _ | CProj _), _ -> false and args_eq (a1,e1) (a2,e2) = Option.equal (eq_located explicitation_eq) e1 e2 && @@ -188,7 +190,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) = Option.equal cases_pattern_expr_eq p1 p2 and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) = - List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 && + List.equal (List.equal cases_pattern_expr_eq) p1 p2 && constr_expr_eq e1 e2 and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) = @@ -260,7 +262,6 @@ let local_binders_loc bll = match bll with (* Legacy functions *) let down_located f (_l, x) = f x -let located_fold_left f x (_l, y) = f x y let is_constructor id = try Globnames.isConstructRef @@ -292,8 +293,7 @@ let ids_of_pattern = let ids_of_pattern_list = List.fold_left - (located_fold_left - (List.fold_left (cases_pattern_fold_names Id.Set.add))) + (List.fold_left (cases_pattern_fold_names Id.Set.add)) Id.Set.empty let ids_of_cases_indtype p = @@ -367,6 +367,8 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (_,_) -> Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc + | CProj (_,c) -> + f n acc c ) let free_vars_of_constr_expr c = @@ -448,6 +450,8 @@ let map_constr_expr_with_binders g f e = CAst.map (function let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in let d' = f e'' d in (id,bl',t',d')) dl) + | CProj (p,c) -> + CProj (p, f e c) ) (* Used in constrintern *) @@ -571,7 +575,7 @@ let expand_binders ?loc mkC bl c = let c = CAst.make ?loc @@ CCases (LetPatternStyle, None, [(e,None,None)], - [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))]) + [(Loc.tag ?loc:loc1 ([[p]], c))]) in (ni :: env, mkC ?loc ([id],Default Explicit,ty) c) in |