diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 16:19:51 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 14:59:26 +0100 |
| commit | a1aff01d16bad2f44392fd5cb804092e12e558ed (patch) | |
| tree | bd2a1faf08b1c399171a308cf45bfd46d60ab5c5 /interp/topconstr.ml | |
| parent | 78bad016e389cd78635d40281bfefd7136733b7e (diff) | |
CLEANUP: removing unused field
I have removed the second field of the "Constrexpr.CRecord" variant
because once it was set to "None"
it never changed to anything else.
It was just carried and copied around.
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 15ac46e29..837630183 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -116,7 +116,7 @@ let fold_constr_expr_with_binders g f n acc = function | CDelimiters (loc,_,a) -> f n acc a | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> acc - | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l + | CRecord (loc,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l | CCases (loc,sty,rtnpo,al,bl) -> let ids = ids_of_cases_tomatch al in let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in @@ -218,7 +218,7 @@ let map_constr_expr_with_binders g f e = function | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ as x -> x - | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l) + | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l) | CCases (loc,sty,rtnpo,a,bl) -> (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in |