diff options
| author | Matej Kosik | 2015-12-16 16:19:51 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-01-11 14:59:26 +0100 |
| commit | a1aff01d16bad2f44392fd5cb804092e12e558ed (patch) | |
| tree | bd2a1faf08b1c399171a308cf45bfd46d60ab5c5 /interp/constrintern.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/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 68bc0b1092..c0203b0666 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1479,7 +1479,7 @@ let internalize globalenv env allow_patvar lvar c = apply_impargs c env impargs args_scopes (merge_impargs l args) loc - | CRecord (loc, _, fs) -> + | CRecord (loc, fs) -> let cargs = sort_fields true loc fs (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l) |